私のブックマーク
私のブックマーク:SAT ソルバー
番原 睦則 (神戸大学 情報基盤センター)
宋 剛秀 (神戸大学 情報基盤センター)
田村 直之 (神戸大学 情報基盤センター)
井上 克巳 (国立情報学研究所)
はじめに
命題論理の充足可能性判定問題 (SAT) は,与えられた命題論理式の充足可能性を判定する問題であり,最初にNP完全性が証明された問題でもある.SAT は人工知能および計算機工学における最も基本的な問題として,論理合成,システム検証,プランニング問題,スケジューリング問題,制約充足問題,制約最適化問題,定理証明など,さまざまな分野に応用されている.近年,106-107 個の変数をもつ大規模な SAT問題を,非常に高速に解くことが可能な SAT ソルバーが実現され,これらの分野への実用的応用が急速に拡大している.
このように,与えられた問題を論理式で表現し SAT ソルバーを用いて解くことから,SAT 技術は現代の推論システムにおいて基盤的役割を果たしているといえる.本稿では,こうしたSAT技術のなかでも中心的な役割を果たしている SAT ソルバーについて,筆者らが参加した CSPSAT プロジェクト及びその発展である CSPSAT2 プロジェクト(以下,まとめて CSPSAT プロジェクトと呼ぶ) の活動を含め,有用な Webページを紹介する.なお SAT に関するポータルサイトとしては,SAT Live! — http://www.satlive.org/があるので,参照していただきたい.
CSPSAT プロジェクト
CSPSAT プロジェクト —http://www.edu.kobe-u.ac.jp/istc-tamlab/cspsat/の目的は,制約最適化問題,制約充足問題,および,それらを拡張した問題について,問題をSAT 符号化 (論理式で表現) し SAT ソルバーを用いて解く手法に着目し,実用的規模の問題を高速に解くための手法の研究,実証ソフトウェアの開発,および評価を行うことである.
本プロジェクトは JSPS 科研費 20240003, 24300007 の助成を受けたものである.
ここでは,CSPSAT プロジェクトの成果のうち,本学会誌の特集とソフトウェアを紹介する.
特集「最近のSAT技術の発展」 人工知能学会誌 第25巻 第1号 (2010年1月)
本特集は以下の8篇の解説から構成されている.読者にはまず,井上・田村による特集「最近のSAT技術の発展」にあたって — http://bach.istc.kobe-u.ac.jp/aisat.htmlで概要を把握した後に,各論を読んでいただくことをお勧めする.
- SATソルバーの基礎,井上克巳,田村直之,人工知能学会誌,25巻1号,pp.57-67,2010年 —http://ci.nii.ac.jp/naid/110007504953
- 高速SATソルバーの原理,鍋島英知,宋剛秀,人工知能学会誌,25巻1号,pp.68-76,2010年 — http://ci.nii.ac.jp/naid/110007504954
- 制約最適化問題とSAT符号化,田村直之,丹生智也,番原睦則,人工知能学会誌,25巻1号,pp.77-85,2010年 — http://ci.nii.ac.jp/naid/110007504955
- SMT:個別理論を取り扱うSAT技術,岩沼宏治,鍋島英知,人工知能学会誌,25巻1号,pp.86-95,2010年 — http://ci.nii.ac.jp/naid/110007504956
- モデル列挙とモデル計数,長谷川隆三,藤田博,越村三幸,人工知能学会誌,25巻1号,pp.96-104,2010年 — http://ci.nii.ac.jp/naid/110007504957
- *-SAT: SATの拡張,平山勝敏,横尾真,人工知能学会誌,25巻1号,pp.105-113,2010年 — http://ci.nii.ac.jp/naid/110007504958
- SATによるプランニングとスケジューリング,鍋島英知,人工知能学会誌,25巻1号,pp.114-121,2010年 — http://ci.nii.ac.jp/naid/110007504959
- SATによるシステム検証,番原睦則,田村直之,人工知能学会誌,25巻1号,pp.122-129,2010年 — http://ci.nii.ac.jp/naid/110007504960
ソフトウェア成果物
CSPSAT プロジェクトにおいて開発された主なソフトウェアとしては,以下のものがある.
- GlueMiniSat —https://sites.google.com/a/nabelab.org/glueminisat/home
by 鍋島英知 (山梨大学) — http://www.nabelab.org/GlueMiniSat は,SAT ソルバーの劇的な性能向上と普及に貢献した代表的なソルバーMiniSatを改良した系統的ソルバーである.SAT Competition 2011 の Application 部門において,逐次型ソルバーとしてUNSAT
クラスで優勝,SAT+UNSAT
クラスで準優勝するなど,優秀な成績をおさめている. - QMaxSAT —http://sites.google.com/site/qmaxsat/
by 越村三幸 (九州大学・長谷川研究室) —http://hyoka.ofc.kyushu-u.ac.jp/search/details/K000184/
MaxSAT とは SAT を最適化問題に拡張したものである.QMaxSAT はMiniSat を改良した MaxSAT ソルバーである.MaxSAT Evaluation 2011-2012 の Partial MaxSAT 部門において優秀な成績をおさめている. - Sugar —http://bach.istc.kobe-u.ac.jp/sugar/
by 田村直之 (神戸大学) — http://bach.istc.kobe-u.ac.jp/tamura-jp.html
Sugar は,制約充足問題,制約最適化問題,最大制約充足問題を解くことができる SAT ベースの制約ソルバーである.CSP Solver Competition 2008-2009 において,二年連続・複数部門で優勝している. - Copris —http://bach.istc.kobe-u.ac.jp/copris/
by 田村直之 (神戸大学) — http://bach.istc.kobe-u.ac.jp/tamura-jp.html
Copris は,オブジェクト指向言語と関数型言語が融合された Scala 上の制約プログラミング用 DSL (Domain-Specific Language) である.バックエンドの制約ソルバーとしてSugarを用いており,制約ソルバーとしての性能も高い.
ソルバー
SAT は典型的な組合せ問題であり,SAT を解くための多くのアルゴリズムとソルバーが開発されてきた.これらの SAT ソルバーを大別すると,系統的ソルバー (systematic solver) と,確率的ソルバー (stochastic solver) の二種類が存在する.系統的ソルバーは,系統的探索 (systematic search) を行う完全な(complete) アルゴリズムに基づいており,SAT 問題の充足可能性と充足不能性のいずれも判定可能である.SAT 問題が充足不能であるとき,系統的ソルバーはすべての可能な真偽値割り当てに相当する探索を行った後にUNSAT
と判定して終了する.これに対し確率的ソルバーは,確率的局所探索 (stochastic local search)を行う不完全な (incomplete) アルゴリズムに基づいており,充足可能性は判定可能であるが充足不能性は一般に判定できない.ポートフォリオ型ソルバーは一般に複数のソルバーを組み合わせて SAT 問題を解くソルバーである.経済学からのアイデアであるポートフォリオ戦略を用いることで,解を見つけられないリスクと探索の効率化のトレードオフを最適化することができる.
系統的ソルバー
- MiniSat —http://minisat.se/
by Niklas Eén — http://een.se/niklas/ and Niklas Sörensson
矛盾解析,監視リテラル,バックジャンプ法,変数選択ヒューリスティックス,ランダム・リスタート戦略などの高速化技術を効率良く実装し,SAT ソルバーの劇的な性能向上と普及に貢献した代表的なソルバー.ソースコードリポジトリ— https://github.com/niklasso/minisatから最新のソースコードが入手可能. - Glucose — http://www.lri.fr/~simon/?page=glucose
by Gilles Audemard and Laurent Simon
Minisat 系のソルバー.SAT 問題を解く過程で大量に生成される学習節の評価尺度としてLiterals Blocks Distance (LBD) を導入し,SAT ソルバーの基本動作である単位伝搬を促進する学習節を獲得・保持するように工夫されている. - GlueMiniSat —https://sites.google.com/a/nabelab.org/glueminisat/home
by 鍋島英知 (山梨大学) — http://www.nabelab.org/
充足不能性の判定に優れた Minisat 系のソルバー.学習節の評価尺度として Glucoseで採用された LBD を強化した Strict LBD を導入し,単位伝搬を促進する学習節を獲得・保持し,さらに,より良い学習節の獲得を促すため非常に積極的なリスタート戦略をとっている. - Lingeling —http://fmv.jku.at/lingeling/,PrecoSAT —http://fmv.jku.at/precosat/,PicoSAT —http://fmv.jku.at/picosat/
by Armin Biere —http://fmv.jku.at/biere/
MiniSat 同様,SAT ソルバーの劇的な性能向上と普及に貢献した代表的なソルバー群.開発者の Armin Biere 教授は,SAT ソルバーの工学的応用の中で最も成功したものの一つである有界モデル検査 (bounded model checking) の研究でも著名. - clasp —http://potassco.sourceforge.net/
by Torsten Schaub 他 — http://www.cs.uni-potsdam.de/~torsten/
SAT ソルバーの高速化技術を取り入れた解集合ソルバー.系統的ソルバーとしても利用可能. - SAT4J —http://www.sat4j.org
by Daniel Le Berre 他 — http://www.cril.univ-artois.fr/~leberre/
Java で実装された Minisat 系のソルバー.MaxSAT ソルバー,擬似ブールソルバーとしても利用可能. - zChaff —http://www.princeton.edu/~chaff/zchaff.html
- BerkMin —http://eigold.tripod.com/BerkMin.html
確率的ソルバー
- Walksat —http://www.cs.rochester.edu/u/kautz/walksat/
by Bart Selman —http://www.cs.cornell.edu/selman/and Henry Kautz —
http://www.cs.rochester.edu/u/kautz/
Walksat の最新のソースコードが入手可能.また,GSAT のオリジナルソースコードも公開されている. - UBCSAT —http://ubcsat.dtompkins.com/
by ß-Lab, The University of British Columbia —http://www.cs.ubc.ca/labs/beta/
これまで SAT, CP などの国際会議で発表された様々な確率的局所探索アルゴリズムを利用可能.
ポートフォリオ型 & 並列ソルバー
- SATzilla —http://www.cs.ubc.ca/labs/beta/Projects/SATzilla/
by Kevin Leyton-Brown 他 — http://www.cs.ubc.ca/~kevinlb/ - ppfolio —http://www.cril.univ-artois.fr/~roussel/ppfolio/
by Olivier Roussel —http://www.cril.univ-artois.fr/~roussel/index.php?lang=eng - Plingeling —http://fmv.jku.at/lingeling/
by Armin Biere —http://fmv.jku.at/biere/ - ManySAT —http://www.cril.univ-artois.fr/~jabbour/manysat.htm
by Youssef Hamadi 他 — http://research.microsoft.com/en-us/people/youssefh/
MaxSAT ソルバー,擬似ブールソルバー,制約ソルバー,SMT ソルバー
- QMaxSAT —http://sites.google.com/site/qmaxsat/
by 越村三幸 (九州大学・長谷川研究室) —http://hyoka.ofc.kyushu-u.ac.jp/search/details/K000184/
Minisat 系の MaxSAT ソルバー. - MiniSat+ — http://minisat.se/
by Niklas Eén — http://een.se/niklas/ and Niklas Sörensson
Minisat 系の擬似ブールソルバー. - Sugar —http://bach.istc.kobe-u.ac.jp/sugar/
by 田村直之 (神戸大学) — http://bach.istc.kobe-u.ac.jp/tamura-jp.html
SATベースの制約ソルバー. - Z3 —http://z3.codeplex.com/
by Microsoft Research — http://research.microsoft.com/en-us/
Satisfiability Modulo Theories Competition 2011 において,複数部門で優勝した高速 SMT ソルバー.
競技会
SAT ソルバーの性能を実用面で評価する場として,国際会議 SAT 2002 以降に,SAT Competition と呼ばれる競技会が併設開催されるようになった.SAT Competition は 2002 〜 2005 年まで毎年開催され,以降は隔年開催となったものの,開催されなかった年には SAT Race と呼ばれる競技会が行われている.2012年は SAT Challenge と呼ばれる新しい競技会が開催された.SAT を解くためのヒューリスティックスに関しては,膨大な量の研究論文が出版されているものの,アルゴリズム相互の比較は理論面だけでは難しく論文からは実用面における指針が得られないことが多い.競技会は SAT ソルバーを工学レベルでサポートし,各ソルバーの経験的評価を容易にし,各々の得意・不得意と限界を明らかにしてくれる.さらに,このような会に参加することで開発者の研究意欲も刺激し,人材育成にもつながっている.また,競技会向けに厳選される問題が,競技終了後もソルバー開発のためのベンチマーク問題としてSATLIB 問題とともに使用され続けている
SAT Competition, SAT Race, SAT Challenge の3つの競技会はそれぞれルールが違うため,本稿では最も歴史のある SAT Competition について簡単に説明する.
競技会では,ベンチマーク問題のタイプによって3部門に分かれて競い合う.
- Application 部門:モデル検査,プランニング,暗号など,多様な応用問題のインスタンスを集めたもの.最も重視されている部門.
- Random 部門:ランダム k-SAT 問題のインスタンスだけを集めたもの.
- Crafted 部門:その他の問題すべてを扱う.
それぞれの部門で,問題の充足可能性を示す SAT
,問題の充足不能性を示す UNSAT
,どちらのタイプの問題もあってモデルの有無を判定する SAT+UNSAT
,の3種類に分かれて競い合う.UNSAT
であることを示す問題では完全な探索を必要とするため,SAT
であることを示す問題よりも一般に難しいとされる.
SAT Competition 2011 の金メダリスト (CPU時間での評価結果)
Application | Crafted | Random | |
---|---|---|---|
SAT+UNSAT | Glucose | 3S | 3S |
SAT | contrasat | ppfolio | sparrow2011 |
UNSAT | GlueMiniSat | clasp | march_rw |
SAT Competition 2011 で優勝したソルバーを上の表に示す.SAT Competition 2011 は過去の競技会と異なり,逐次ソルバー,並列ソルバー,ポートフォリオ型ソルバーを区別することなく,CPU時間と WC (Wall Clock) 時間の2つに分けて評価している.上の表は CPU時間 での評価結果である.
Application 部門において,Glucose,contrasat,GlueMiniSatは Minisat 系と呼ばれる MiniSatを改良した系統的ソルバーである.Crafted 部門において,3S (Satisfiability Solver Selector),ppfolioはポートフォリオ型ソルバー,claspは解集合ソルバーでもある系統的ソルバーである.Random 部門の sparrow2011 は確率的ソルバー,march_rw は系統的ソルバーである.ほかに特別部門として,Best Minisat Hack 部門で Minisat 系の CIR_MiniSAT が優勝した.
この結果から,問題のタイプによって得意・不得意が出ていることがわかる.優勝者もほぼ分散している.Minisat 系は Application 部門を独占しており,実際の応用問題に強いソルバーである.ポートフォリオ型 は 3部門で優勝しており,平均的な強みがある万能型のソルバーである.また,WC 時間 での評価では,優勝者の殆どをポートフォリオ型が占める.
SAT Competitions — http://www.satcompetition.org/
- SAT Competition 2011 — http://www.satcompetition.org/2011/
- SAT Competition 2009 — http://www.satcompetition.org/2009/
- SAT Competition 2007 — http://www.satcompetition.org/2007/
- SAT Competition 2005 — http://www.satcompetition.org/2005/
- SAT Competition 2004 — http://www.satcompetition.org/2004/
- SAT Competition 2003 — http://www.satcompetition.org/2003/
- SAT Competition 2002 — http://www.satcompetition.org/2002/
SAT-Race
- SAT-Race 2010 — http://baldur.iti.uka.de/sat-race-2010/
- SAT-Race 2008 — http://baldur.iti.uka.de/sat-race-2008/
- SAT-Race 2006 — http://fmv.jku.at/sat-race-2006/
SAT Challenge
- SAT Challenge 2012 — http://baldur.iti.kit.edu/SAT-Challenge-2012/
SAT 関連の競技会
MaxSAT,限量ブール式 (QBF),擬似ブール (Pseudo-Boolean) など SAT の重要な拡張についても,ソルバーの性能を評価する競技会がある.SAT技術と関連の深い,制約充足問題 (CSP) を解く制約ソルバー,Satisfiability Modulo Theories (SMT) ソルバー,解集合 (ASP) ソルバー の競技会とあわせて紹介する.
- MaxSAT Evaluation —http://maxsat.ia.udl.cat/
2006年から毎年開催されている MaxSAT ソルバーの性能を評価する競技会. - Pseudo-Boolean Competition —http://www.cril.univ-artois.fr/PB12/
2005年から (2008年を除き) 毎年開催されている擬似ブールソルバーの性能を評価する競技会. - QBF Solver Evaluation — http://www.qbflib.org/index_eval.php
2004年から (2009年と2011年を除き) 毎年開催されている QBF ソルバーの性能を評価する競技会. - CSP Solver Competition — http://www.cril.univ-artois.fr/CSC09/
2005-2006,2008-2009 に開催された制約ソルバーの性能を評価する競技会. - Satisfiability Modulo Theories Competition (SMT-COMP) —http://www.smtcomp.org/
2005年から毎年開催されている SMT ソルバーの性能を評価する競技会. - ASP Competition —https://www.mat.unical.it/aspcomp2013/
2007年から隔年開催されている解集合ソルバーの性能を評価する競技会.
ハンドブック・解説・スライド
ハンドブック
- Biere, A., Heule, M. J. H., Maaren, van H., and Walsh, T. eds.: Handbook of Satisfiability,Vol.185 of Frontiers in Artificial Intelligence and Applications, IOS Press (2009) — http://www.iospress.nl/book/handbook-of-satisfiability/
これまでの SAT 技術について幅広く説明されている.ぜひ参照していただきたい.
解説
上記人工知能学会誌特集以外の最近の解説・レビューでは,以下のものがある.
- Gomes, C. P., Kautz, H., Sabharwal, A., and Selman, B.: Satisfiability Solvers, in Handbook of Knowledge Representation, Vol.3 of Foundations of Artificial Intelligence, pp.89-134,Elsevier (2008) —http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-Handbook.pdf
- Malik, S. and Zhang, L.:
Boolean satisfiability — from theoretical hardness to practical success,Communications of the ACM,
Vol.52, No.8, pp.76-82 (2009)—http://dl.acm.org/citation.cfm?id=1536637 - 梅村晃広 :SAT ソルバ・SMT ソルバの技術と応用,コンピュータソフトウェア,27巻3号,pp.24-35,(2010)—http://ci.nii.ac.jp/naid/10026562857
スライド,ビデオ
- Donald E. Knuth :Satisfiability and The Art of Computer Programming,The 15th International Conference on Theory and Applications of Satisfiability Testing,invited talk (2012)—http://www-cs-faculty.stanford.edu/~uno/sat2012.pdf
Donald E. Knuth 先生によるSAT 2012 — http://sat2012.fbk.eu/の招待講演のスライド. - First International SAT/SMT Solver Summer School 2011 —https://wikis.mit.edu/confluence/display/satsmtschool11/SATSMT+Summer+School+2011
2011年に MIT で開催された第1回 SAT ソルバー/SMT ソルバー国際サマースクール.講演者は世界中から集まった第一線の研究者.講演スライドが公開されているので,ぜひ参照していただきたい. - Second International SAT/SMT Solver Summer School 2012—http://satsmtschool2012.fbk.eu
国際サマースクールの第2回目.講演のビデオが公開されている.
ジャーナル,国際会議
ジャーナル
- Journal on Satisfiability, Boolean Modeling and Computation (JSAT) — http://www.iospress.nl/journal/journal-on-satisfiability-boolean-modeling-and-computation/
- Constraints —http://www.springerlink.com/content/100252/
- Artificial Intelligence — http://www.journals.elsevier.com/artificial-intelligence/
- Journal of Automated Reasoning —http://www.springer.com/computer/theoretical+computer+science/journal/10817
- Journal of Artificial Intelligence Research (JAIR) —http://www.jair.org/
国際会議・国際ワークショップ
- SAT: International Conference on Theory and Applications of Satisfiability Testing — http://www.satisfiability.org/
- CP: International Conference on Principles and Practice of Constraint Programming — http://www.cp2012.org
- CPAIOR: International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems — http://www.andrew.cmu.edu/user/vanhoeve/cpaior/
- ECAI: European Conference on Artificial Intelligence — http://www2.lirmm.fr/ecai2012/
- AAAI: AAAI Conference on Artificial Intelligence — http://www.aaai.org/Conferences/conferences.php
- IJCAI: International Joint Conference on Artificial Intelligence — http://ijcai.org/
- LPAR: International Conference on Logic for Programming Artificial Intelligence and Reasoning — http://www.computational-logic.org/lpar-17/Home.html
- IJCAR: International Joint Conference on Automated Reasoning — http://www.ijcar.org/
- CADE: International Conference on Automated Deduction — http://www.cadeinc.org/
- CAV: International Conference on Computer Aided Verification — http://cav2013.forsyte.at/
- DAC: Design Automation Conference — http://www.dac.com/
- PoS : International Workshop on Pragmatics of SAT — http://www.satcompetition.org/PoS12/
パズル好きの方へ
SAT ソルバーを使ってパズルを解きたい場合,問題を命題論理式で表現する必要がある.しかし,論理パズルなど自然に書ける問題を除くと,その作業は容易ではない.実際,競技会で用いられる問題のほとんどは,より複雑な応用問題から SAT 問題に変換されて作られたものである.以下は,SAT ソルバーを使ってパズルを解いてみたいが,問題を命題論理式で表現するのはちょっと,という方にお勧めである.
- パズルをSugar制約ソルバーで解く —http://bach.istc.kobe-u.ac.jp/sugar/puzzles/
by 田村直之 (神戸大学) — http://bach.istc.kobe-u.ac.jp/tamura-jp.html - プログラム不要の「制約プログラミング手習い」—http://karetta.jp/book-cover/withoutprogramming/
by 藤原博文 (タイムインターメディア) —http://www.pro.or.jp/~fuji/
おわりに
本稿では,近年,ますますその重要性を増してきている SAT 技術の中から,SAT ソルバーを中心に有用と思われるリソースを紹介した.本稿が一人でも多くの読者の方々の興味を引き,何らかの SAT 関連の研究の参考あるいは引き金になれば幸いである.