ソフトウェア科学特論

Table of Contents

概要

目標

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

対象

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

担当者

  • 田村直之

オフィスアワー

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

成績評価方法

BEEF を通じて提出される以下の課題およびレポートで評価する.

  • 講義中の課題
  • 最終レポート

注意

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

スケジュール

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

2017 日程表

日時教室
1 2017-06-13 TueC2-201, 第2演習室
2 2017-06-15 Thu第2演習室
3 2017-06-20 Tue第2演習室
4 2017-06-22 Thu第2演習室
5 2017-06-27 Tue第2演習室
6 2017-06-29 Thu第2演習室
7 2017-07-04 Tue第2演習室
8 2017-07-06 Thu第2演習室
9 2017-07-11 Tue第2演習室
10 2017-07-13 Thu第2演習室
11 2017-07-18 Tue第2演習室
12 2017-07-20 Thu第2演習室
13 2017-07-25 Tue第2演習室
14 2017-07-27 Thu第2演習室
15 2017-08-01 Tue第2演習室 (予備日)
16 2017-08-03 Thu休講 (試験期間)
17 2017-08-08 Tue休講 (試験期間)

テキスト

内容 (予定)

DONE 1W 2017-06-13 Tue

講義

演習

  • 演習1-1
    • テキスト「命題論理」の「3.6 練習問題」の問1に解答せよ(BEEF).

宿題

DONE 1W 2017-06-15 Thu

講義

演習

  • 演習1-2
    • テキスト「命題論理」の「4.2 練習問題」の問2に解答せよ(BEEF).
  • 演習1-3
    • テキスト「命題論理」の「4.2 練習問題」の問4に解答せよ(BEEF).
  • 演習1-4
    • テキスト「命題論理」の「4.8 練習問題」の問2に解答せよ(BEEF).
  • 演習1-5
    • テキスト「命題論理」の「4.8 練習問題」の問8に解答せよ(BEEF).
  • 演習1-6
    • テキスト「命題論理」の「4.8 練習問題」の問9に解答せよ(BEEF).

DONE 2W 2017-06-20 Tue

演習

  • 演習2-1
    • テキスト「命題論理」の「4.11.4 練習問題」の問2に解答せよ(BEEF).

DONE 2W 2017-06-22 Thu

CLOSED: 2017-06-23 Fri 14:50

演習

  • 演習2-2
    • テキスト「命題論理の推論体系」の「4.3.2 練習問題」の問1の解答例にならって問3に解答せよ(BEEF).
  • 演習2-3
    • テキスト「命題論理の推論体系」の「4.3.2 練習問題」の問1の解答例にならって問4に解答せよ(BEEF).
  • 演習2-4
    • SATソルバーとその応用についてWebで検索し調べ, 自分が興味を持った応用について簡単に説明せよ(BEEF).
  • 演習2-5
    • The SAT Gameを試せ.

宿題

  • 『TAOCP 7.2.2.2 Satisfiability』の該当部分を読んでおくこと.

DONE 3W 2017-06-27 Tue

演習

  • 演習3-1
    • sat13をインストールし,sample.satに対する解を求めよ.

宿題

  • 『TAOCP 7.2.2.2 Satisfiability』の該当部分を読んでおくこと.

DONE 3W 2017-06-29 Thu

講義

演習

  • 演習3-2
    • (式1)の \(F\) に対する入力ファイルを答えよ(BEEF).
  • 演習3-3
    • (式2)の \(G\) に対する入力ファイルを答えよ(BEEF).
  • 演習3-4
    • (式2)の \(G\) から融合原理で空節を導出せよ(BEEF).
  • 演習3-5
    • テキストの「3.3.2 練習問題」の問1のsat13での実行結果を示せ(BEEF).
  • 演習3-6
    • テキストの「3.3.2 練習問題」の問5に対する入力ファイルを答えよ(BEEF).

宿題

  • 『TAOCP 7.2.2.2 Satisfiability』の該当部分を読んでおくこと.

DONE 4W 2017-07-04 Tue

講義

演習

  • 演習4-1
    • \(\textit{waerden}(3,4;17)\) の解の1つを求めよ(BEEF).
  • 演習4-2
    • テキストの「4.1.2 練習問題」の問7に解答せよ(BEEF).
  • 演習4-3
    • テキストの「4.1.2 練習問題」の問9の資料を読め.

宿題

  • 『TAOCP 7.2.2.2 Satisfiability』の該当部分を読んでおくこと.

DONE 4W 2017-07-06 Thu

講義

演習

  • 演習4-4
    • テキストの「4.1.2 練習問題」の問8の節数を答えよ(BEEF).
  • 演習4-5
    • テキストの「4.1.2 練習問題」の問8の入力ファイルを答えよ(BEEF).

宿題

  • 『TAOCP 7.2.2.2 Satisfiability』の該当部分を読んでおくこと.

DONE 5W 2017-07-11 Tue

演習

  • 演習5-1
    • テキストの「4.2.2 練習問題」の問4で \(n=4\) の場合のsat13の出力結果を示せ(BEEF).
  • 演習5-2
    • 上の出力結果はどのようなLangford pair列を表しているか(BEEF).
  • 演習5-3
    • 4クイーン問題で \(i\) 行 \(j\) 列のクイーンの有無を \(x_{ij}\) で表す(\(i,j=1,2,3,4\)). 4クイーン問題の条件はどのような数式で表されるか(BEEF).

宿題

  • 『TAOCP 7.2.2.2 Satisfiability』の該当部分を読んでおくこと.

DONE 5W 2017-07-13 Thu

演習

  • 演習5-4
    • テキストの「4.3.2 練習問題」の問1の実行結果で,どの領域がどの色で彩色されたか答えよ(BEEF).
  • 演習5-5
    • テキストの「4.3.2 練習問題」の問2の実行で,sat13の実行にかかったCPU時間を答えよ(BEEF).
  • 演習5-6

DONE 6W 2017-07-18 Tue

最終レポート

  • 最終レポートをパワーポイント等で作成し,期限までにBEEFから提出すること.
  • 7月25日(火)または7月27日(木)に最終レポートのプレゼン(10分程度)を行うこと.
  • 最終レポートのタイトル例
    • 「SATソルバーを用いた数独の解法」
    • 「SATソルバーを用いたナンバーリンクの解法」
    • 「SATソルバーを用いたXXXの解法」
  • 最終レポートの構成例
    1. 表紙
      • タイトル,所属,学籍番号,氏名
    2. 「XXXとは」
      • 問題の説明
    3. 「XXXのSAT符号化」
      • 問題をCNFに変換する方法の説明
    4. 「実行結果」
      • 具体的な問題のSATソルバーでの実行結果(節数やCPU時間など)
    5. 「考察」
    6. 「結論」

演習

  • 演習6-1
    • 最終レポートのタイトルとプレゼン希望日を回答してください(BEEF,7/24締め切り).

DONE 6W 2017-07-20 Thu

最終レポート

  • 最終レポート作成に取り組む

7W 2017-07-25 Tue

最終レポート

  • 最終レポート作成に取り組む
  • 該当者による最終レポートのプレゼン

7W 2017-07-27 Thu

最終レポート

  • 該当者による最終レポートのプレゼン

Date: 2017-07-20 23:52:31 JST

Author: 田村直之

Org version 7.8.02 with Emacs version 24

Validate XHTML 1.0