充足可能性問題とSATソルバ
論理学から知能にアプローチ：いかにして機械は問題を解くか
このような学問です
SATソルバは、充足可能性問題(SAT問題)を解くソフトウェアで、様々な制約解消問題を論理式にエンコードすることによりSATソルバで高速に解けることが知られています。
社会での応用先はこのような分野です
SATソルバ製品の構成管理（カスタマイズの組み合わせ）が膨大な数に上る際の探索や、ソフトウェアやハードウェアの有界モデル検査と呼ばれる品質保証技術に用いられています。
このような講義内容です
SAT/SMTソルバを用いた問題解決技法を習得します。SAT/SMTソルバとしてZ3,miniSAT等やグラフィカルな処理系としてAlloyを用います。また、CDCLアルゴリズムの学習挙動を始めとしたSATソルバの内部動作についても理解することを目指します。
講義方法に特徴があります
様々な問題のSATソルバによる解法を実際に体験し、自らの問題へと応用するための力を培います。
所属 ： 工学部電気電子・情報工学科 情報コース
講師 ： 助教 今井 敬吾
プログラミング言語理論を専門とし、様々なプログラミングパラダイムの産業応用に興味を持つ。著書にScala実践プログラミング (秀和システム)、型システム入門(オーム社、共訳)がある。
