Vol.28 No.2 (2013/03) SAT ソルバー

私のブックマーク

私のブックマーク：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で概要を把握した後に，各論を読んでいただくことをお勧めする．

  1. SATソルバーの基礎，井上克巳，田村直之，人工知能学会誌，25巻1号，pp.57-67，2010年 —http://ci.nii.ac.jp/naid/110007504953
  2. 高速SATソルバーの原理，鍋島英知，宋剛秀，人工知能学会誌，25巻1号，pp.68-76，2010年 — http://ci.nii.ac.jp/naid/110007504954
  3. 制約最適化問題とSAT符号化，田村直之，丹生智也，番原睦則，人工知能学会誌，25巻1号，pp.77-85，2010年 — http://ci.nii.ac.jp/naid/110007504955
  4. SMT：個別理論を取り扱うSAT技術，岩沼宏治，鍋島英知，人工知能学会誌，25巻1号，pp.86-95，2010年 — http://ci.nii.ac.jp/naid/110007504956
  5. モデル列挙とモデル計数，長谷川隆三，藤田博，越村三幸，人工知能学会誌，25巻1号，pp.96-104，2010年 — http://ci.nii.ac.jp/naid/110007504957
  6. ＊-SAT: SATの拡張，平山勝敏，横尾真，人工知能学会誌，25巻1号，pp.105-113，2010年 — http://ci.nii.ac.jp/naid/110007504958
  7. SATによるプランニングとスケジューリング，鍋島英知，人工知能学会誌，25巻1号，pp.114-121，2010年 — http://ci.nii.ac.jp/naid/110007504959
  8. SATによるシステム検証，番原睦則，田村直之，人工知能学会誌，25巻1号，pp.122-129，2010年 — http://ci.nii.ac.jp/naid/110007504960

ソフトウェア成果物

CSPSAT プロジェクトにおいて開発された主なソフトウェアとしては，以下のものがある．

ソルバー

SAT は典型的な組合せ問題であり，SAT を解くための多くのアルゴリズムとソルバーが開発されてきた．これらの SAT ソルバーを大別すると，系統的ソルバー (systematic solver) と，確率的ソルバー (stochastic solver) の二種類が存在する．系統的ソルバーは，系統的探索 (systematic search) を行う完全な(complete) アルゴリズムに基づいており，SAT 問題の充足可能性と充足不能性のいずれも判定可能である．SAT 問題が充足不能であるとき，系統的ソルバーはすべての可能な真偽値割り当てに相当する探索を行った後にUNSAT と判定して終了する．これに対し確率的ソルバーは，確率的局所探索 (stochastic local search)を行う不完全な (incomplete) アルゴリズムに基づいており，充足可能性は判定可能であるが充足不能性は一般に判定できない．ポートフォリオ型ソルバーは一般に複数のソルバーを組み合わせて SAT 問題を解くソルバーである．経済学からのアイデアであるポートフォリオ戦略を用いることで，解を見つけられないリスクと探索の効率化のトレードオフを最適化することができる．

系統的ソルバー

確率的ソルバー

ポートフォリオ型 & 並列ソルバー

MaxSAT ソルバー，擬似ブールソルバー，制約ソルバー，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-Race

SAT Challenge

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 技術について幅広く説明されている．ぜひ参照していただきたい．

解説

上記人工知能学会誌特集以外の最近の解説・レビューでは，以下のものがある．

スライド，ビデオ

ジャーナル，国際会議

ジャーナル

国際会議・国際ワークショップ

パズル好きの方へ

SAT ソルバーを使ってパズルを解きたい場合，問題を命題論理式で表現する必要がある．しかし，論理パズルなど自然に書ける問題を除くと，その作業は容易ではない．実際，競技会で用いられる問題のほとんどは，より複雑な応用問題から SAT 問題に変換されて作られたものである．以下は，SAT ソルバーを使ってパズルを解いてみたいが，問題を命題論理式で表現するのはちょっと，という方にお勧めである．

おわりに

本稿では，近年，ますますその重要性を増してきている SAT 技術の中から，SAT ソルバーを中心に有用と思われるリソースを紹介した．本稿が一人でも多くの読者の方々の興味を引き，何らかの SAT 関連の研究の参考あるいは引き金になれば幸いである．