ソフトウェア科学特論

Table of Contents

概要

目標

ソフトウェアの設計・構築に対する科学的アプローチとして, 数理論理学ソフトウェア との関連に焦点を置き, 命題論理とSATソルバーについて講義と演習を行う.

特に,今年度は Donald E. Knuth著 "The Art of Computer Programming" (TAOCP), 第4巻, 第6分冊 "Satisfiability" を教科書として,SATソルバーとその応用について学習する.

対象

  • システム情報学研究科 情報科学専攻 1年生

担当者

  • 田村直之

オフィスアワー

  • 随時 (事前に連絡のこと)

成績評価方法

以下で評価する.

  • 講義中の課題
  • 最終プレゼンテーション (10分程度)
    • テキストの練習問題中 (★) がついているテーマに取り組み, その内容・結果について発表を行う.

注意

  • 授業をよりよくするための皆さんの提案・アイディアを歓迎します.
  • 授業の内容が理解できないときは遠慮無く質問してください.
  • 情報科学専攻の「ソフトウェア科学特論」という名称の講義ですので, ソフトウェアのインストールといった作業も,当然ながら必要となる場合があります. 計算機およびソフトウェアに興味がない方々の受講はお薦めしません.
  • スライドやテキストの内容は,更新のタイミング等により, 講義中のものとは異なることがあります. また,他に転載はしないでください.

スケジュール

  • 火曜日,木曜日 10:40-12:10
  • 教室: 情報基盤センター分館 2F 第2演習室

2018 日程表

日時教室
1 2018-06-12 Tue第2演習室
2 2018-06-14 Thu第2演習室
3 2018-06-19 Tue第2演習室
4 2018-06-21 Thu第2演習室
5 2018-06-26 Tue第2演習室
6 2018-06-28 Thu第2演習室
7 2018-07-03 Tue第2演習室
8 2018-07-05 Thu休講
9 2018-07-10 Tue第2演習室
10 2018-07-12 Thu第2演習室
11 2018-07-17 Tue第2演習室
12 2018-07-19 Thu第2演習室
13 2018-07-24 Tue第2演習室
14 2018-07-26 Thu第2演習室
15 2018-07-31 Tue予備日
16 2018-08-02 Thu休講 (試験期間)
17 2018-08-07 Tue休講 (試験期間)

テキスト

BEEF を通じて配布する.また,以下が参考資料である.

  1. Knuth先生の『TAOCP 7.2.2.2 Satisfiability』を読む (作成中)
  2. 命題論理
  3. 命題論理の推論体系 (導出原理,融合原理)
  4. 命題論理とSAT

2018年度 内容 (予定)

DONE 1W 2018-06-12 Tue

講義

  • イントロ
  • Knuth先生とTAOCPについて
  • Knuth版SATソルバーのインストールと利用
  • 序文

演習

  1. (BEEF 演習1) 「序文」を読んで,興味を持った文章を取り上げその感想を書け.

宿題

DONE 1W 2018-06-14 Thu

講義

  • 定義
  • Rivestの式

演習

  1. 3.1の練習問題の問1
  2. 3.1の練習問題の問7
  3. 3.1の練習問題の問8
  4. 3.2の練習問題の問1
  5. 3.2の練習問題の問2
  6. 3.2の練習問題の問3
  7. (BEEF 演習2) 3.2の練習問題の問5
    • SATソルバーの2回の実行結果を回答せよ.

宿題

  • テキストの該当部分を事前に読んでおくこと.

DONE 2W 2018-06-19 Tue

講義

  • 単純な例

演習

  1. 4.1の練習問題の問4
  2. (BEEF 演習3) 4.1の練習問題の問7
    • SATソルバーの実行結果を回答せよ.

宿題

  • テキストの該当部分を事前に読んでおくこと.

DONE 2W 2018-06-21 Thu

講義

  • 厳密被覆

演習

  1. 4.2の練習問題の問1
  2. 4.2の練習問題の問2
  3. (BEEF 演習4) Knuth版プログラムを用い \(n=4\) の時の解を探せ.
    • SATソルバーの実行結果を回答せよ.
    • どのような数列が求まったかを回答せよ.

宿題

  • テキストの該当部分を事前に読んでおくこと.

DONE 3W 2018-06-26 Tue

講義

  • グラフ彩色

演習

  1. (BEEF 演習5) 4.3の練習問題の問12

宿題

  • テキストの該当部分を事前に読んでおくこと.

DONE 3W 2018-06-28 Thu

講義

  • 整数の因数分解

演習

  1. (BEEF 演習6) 4.4の練習問題の問10

宿題

  • テキストの該当部分を事前に読んでおくこと.

DONE 4W 2018-07-03 Tue

講義

  • 故障試験

演習

  1. (BEEF 演習7) 4.5の練習問題の問6で, \(q\) が1縮退した故障を発見するパターンを探せ.

宿題

  • テキストの該当部分を事前に読んでおくこと.

DONE (4W 2018-07-05 Thu)

休講

DONE 5W 2018-07-10 Tue

講義

  • Boole関数の学習

演習

  1. taocpsat-prog.zip の再インストール
    $ cd ~/Desktop/taocp-sat
    $ curl -O http://bach.istc.kobe-u.ac.jp/lect/taocp-sat/taocpsat-prog.zip
    $ unzip taocpsat-prog.zip
    $ cd prog
    $ chmod +x taocpsat
    $ mkdir -p target
    $ scalac -d target/taocpsat-1.0.jar src/main/scala/*.scala     
    
  2. (BEEF 演習8) 4.6の練習問題の問1で, \(2P=40\) に対して得られたDNFを回答せよ.

宿題

  • テキストの該当部分を事前に読んでおくこと.

DONE 5W 2018-07-12 Thu

講義

  • 有界モデル検査

演習

  1. (BEEF 演習9) 4.7の練習問題の問3

宿題

  • テキストの該当部分を事前に読んでおくこと.

DONE 6W 2018-07-17 Tue

  • 最終プレゼンテーションのテーマを考える.
  • (BEEF 演習10) 最終プレゼンテーションのテーマの候補を記入する. 

DONE 6W 2018-07-19 Thu

  • 最終プレゼンテーションのテーマを決め,説明する (各自5分程度)
    • 原則として,テキストの練習問題中 (★) がついているテーマから選択すること
  • 最終プレゼンテーションに取り組む

DONE 7W 2018-07-24 Tue

  • 最終プレゼンテーションに取り組む

DONE 7W 2018-07-26 Thu

  • 最終プレゼンテーション (各自10分程度)
  • プレゼンテーション資料をBEEFから提出すること.

Date: 2018-07-26 16:32:33 JST

Author: 田村直之

Org version 7.8.02 with Emacs version 24

Validate XHTML 1.0