| 授業の目的 【日本語】 | | | 本講義では，高品質ソフトウェアを構築するための科学的アプローチとして，命題論理の充足可能性判定(SAT; Boolean Satisfiability)と制約充足問題(CSP; Constraint Satisfaction Problem)について学ぶ。 |
|
|
| 授業の目的 【英語】 | | [This course will be taught in Japanese.]
In this course, we study Boolean Satisfiability (SAT) and Constraint Satisfaction Problem (CSP) as approaches to developing high-quality software. |
|
|
| 到達目標 【日本語】 | | | 本講義では，高品質ソフトウェアを構築するための科学的アプローチとして，命題論理の充足可能性判定(SAT; Boolean Satisfiability)と制約充足問題(CSP; Constraint Satisfaction Problem)について学ぶ。以下に挙げる3つを達成目標とする。(1)SAT/CSPの基礎を理解する。(2)SAT/CSPソルバーの代表的なアルゴリズムを習得する。(3)SAT/CSP技術を現実問題に応用する力を身に付ける。 |
|
|
| 到達目標 【英語】 | | | In this course, we study Boolean Satisfiability (SAT) and Constraint Satisfaction Problem (CSP) as approaches to developing high-quality software. The goal of this course is (1) to understand the foundations of SAT/CSP, (2) to learn some important algorithms of SAT/CSP solvers, and (3) to have an ability to apply SAT/CSP techniques to real-world problems. |
|
|
| 授業の内容や構成 | | 1. 制約充足問題(CSP)
2. CSPソルバー
3. 制約伝播アルゴリズム
4. 命題論理の充足可能性判定(SAT)
5. SATソルバー
6. 矛盾からの節学習
7. 制約充足問題のSAT符号化
授業で出される練習問題を講義時間外で解き，授業内容の理解を深めておくこと。 | 1. Constraint Satisfaction Problem (CSP)
2. CSP solvers
3. Constraint propagation algorithms
4. Boolean Satisfiability (SAT)
5. SAT solvers
6. Conflict driven clause learning
7. Encoding CSP into SAT |
|
|
| 履修条件・関連する科目 | | |
|
| 成績評価の方法と基準 | | | 講義中に与える演習課題の評価30%，期末試験70%，合計100点満点で60点以上を合格とする． | | Exercises(30%), examination(70%) |
|
|
| 教科書・参考書 | | | 必要に応じて配布する。 | | Handouts are provided in the course as necessary. |
|
|
| 課外学習等（授業時間外学習の指示） | | | 講義において説明した内容を理解し，活用できるようにするために課題を与える． | | Exercises are given for better understanding. |
|
|
| 授業開講形態等 | | |
|
| 遠隔授業（オンデマンド型）で行う場合の追加措置 | | |
|