パズルをSugar制約ソルバーで解く
はじめに
ニコリなどによる
様々なパズルを
Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます．
注意
- 制約ソルバーのSugar (A SAT-based Constraint Solver)は，
与えられた制約充足問題(CSP, Constraint Satisfaction Problem)や組合せ最適化問題を
命題論理の充足可能性判定問題(SAT)に符号化(変換)し，
高速のSATソルバー(MiniSat等)を用いて解を求める
SAT型の制約ソルバーです．
SAT符号化手法としては著者らの考案した順序符号化(order encoding)を用いています．
- Sugarは，解が存在するかどうかを判定し，
解が存在すればその解を表示する，という動作が基本ですので，
そのままでは別解を探索する機能はありません．
別解を探索したい場合は，求まった解の否定を条件として追加し，
再度ソルバーを動かす必要があります．
- Sugarは汎用の制約ソルバーですので，
それぞれのパズル用に専用のソルバーを作ったほうが速くなる可能性があります．
しかし，Sugarは非常に高速です．
深く考えずに作った専用ソルバーより速い可能性も高いです．
- 各ページで説明している制約充足問題での表現方法は，
唯一ではありませんし，もっと効率の良い方法もありえます．
また，良く考えたつもりですが，間違っているかもしれません．
ご自分でも良く考えて，ご利用ください．
- 制約ソルバーSugarに問題を解かせるためには，
すべての制約条件をあらかじめ与えておかないといけません．
そのため，結構，面倒な記述となっています．
- Sugarを動かすには，Java 5，Perl 5，MiniSatを
別にインストールしておくことがが必要です．
Windowsを利用されている方は，
下の「SugarをWindows上でCygwinを用いて動かす方法」をご覧ください．
資料等
リンク
余談
- 制約充足問題(CSP)を解く制約ソルバーは，
古くからある技術ですが，近年の計算機の高速化により注目を集めています．
最近の利用例としては，次のものがあります．
- 制約ソルバーSugarで利用しているSATソルバーも古くからある技術です．
最近になってハードウェアやソフトウェアの検証などに
実用的に利用されるようになってきました．
最近のニュースとしては，
統合開発環境のEclipse 3.4のプラグインの依存関係解析に
Java版のSATソルバーである
SAT4Jが使われているそうです．
Naoyuki Tamura
(
Last modified: Tue Jul 6 23:57:15 2010 JST
,
Since June 4, 2008
)