自動推論: 充足可能性

説明

このコースでは、満足可能性 (SAT/SMT) ツールを適用して幅広い問題を解決する方法を学びます。
ポスターの印刷に適用される長方形のフィッティング、問題のスケジュール設定、パズルの解決、プログラムの正しさなど、アプリケーションの特徴を理解するためにいくつかの基本的な例が示されています。また、命題充足可能性の基本的なアプローチとしての解決策、大きな数式をスケールアップするための CDCL フレームワーク、線形不等式に対処するためのシンプレックス法など、基礎となる理論も紹介されています。

このコースを受講するための軽量なアプローチは、講義を視聴し、対応するクイズを行うだけです。トピックの雰囲気をつかむには、これでうまくいくかもしれません。ただし、より興味深いアプローチは、これを基礎として使用して、いくつかの問題 (たとえば、名誉ある課題で提示された問題) に SAT/SMT を自分で適用することです。