computer-science - SAT（ブール充足可能性問題）に関する学習資料

Question

SAT（ブール充足可能性問題）ソルバーで読むのに適したドキュメントは何ですか。Googleで良い資料を見つけることができませんでした。私が見つけたドキュメントは、鳥瞰図、高度すぎる、または破損したPDFファイルのいずれかでした...

最新の実用的なSATソルバーのアルゴリズムについて学ぶために、どの論文/ドキュメントをお勧めしますか？

Answer 1

ウィキペディアのDavis-Putnam-Logemann-Lovelandページには概要があります。

そうすれば、ミニサットペーパー「拡張可能なSATソルバー」に従うことができるはずです。

minisatで使用される競合駆動型学習アルゴリズムを理解するには、「GRASP-充足可能性のための新しい検索アルゴリズム」も読む必要があります。

これらのリソースを使用して、PythonでSATソルバーを非常に簡単に作成できました。私のsat.pyコードは利用可能です（現在LGPL 2.1）が、それはごく最近のものなので、まだバグが含まれている可能性があります。minisat設計からのいくつかの最適化が欠けています。生の速度が必要な場合は、minisatコードを使用してください;-)

更新：OCamlバージョンのsat.mlも作成しました。これにより、タイプが見やすくなる可能性があります。

Answer 2

良い本は次のとおりです。UweSchöning; JacoboTorán-満足度の問題