パズルをSugar制約ソルバーで解く
はじめに ニコリなどによる 様々なパズルを Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます． 数独(Sudoku)パズルをSugar制約ソルバーで解く カックロ(Kakuro, Cross Sums)パズルをSugar制約ソルバーで解く 美術館(Akari, Light Up)パズルをSugar制約ソルバーで解く 四角に切れ(Shiaku)パズルをSugar制約ソルバーで解く ナンバーリンク(Number Link)パズルをSugar制約ソルバーで解く ましゅ(Masyu)パズルをSugar制約ソルバーで解く スリザーリンク(Slitherlink)パズルをSugar制約ソルバーで解く 橋をかけろ(Hashiwokakero)パズルをSugar制約ソルバーで解く (一部作成中) ヤジリン(Yajilin)パズルをSugar制約ソルバーで
SATソルバを使うためにCNFを作る - soutaroブログ
SATソルバっていうのは，充足可能性問題（SATisfiability problem）を解いてくれるソフトウェアのことで，SATソルバで数独を解くとか，以外と身近なところに応用があったりします．SATソルバは数独を解くだけじゃなくて，プログラムの停止性の判定に使うとか，いろいろな応用を考えることができる良いものです．普通，SATソルバはCNFという論理式の特殊な形を取り扱います．日本語だと乗法標準形とか言うらしいですけど，別にこの言葉は忘れても良いと思います．詳しくはWikipediaでも見てもらえれば良いのですが，CNFは，変数かそのnot付けたやつ，をorで結んだやつ，をandで結んだやつ，という意味です． CNF ::= c1 && ... && c2 c ::= l1 || ... || l2 l ::= x | !x 任意の論理式(変数(x)とor(||)とand(&&)と「な
SAT ソルバで数独を解く方法 - まめめも
数独は非常に SAT に変換しやすい問題です。全部参考文献 *1 に載っている内容ですが、なるべくわかりやすく説明してみます。ちょっと長いです。 SAT とは まず SAT をごく簡単に説明します。すでに SAT を知っている人はここは読み飛ばしてください。 命題論理式の形の一つに乗法標準形のというのがあります。変数か変数の否定 (リテラルと言います) を or だけでつないだ式 (節と言います) を and だけでつないだ論理式のことを言います。つまり以下みたいな形です。 ( a1 or !a2 or ... or an) and ( b1 or !b2 or ... or !bn) and ... and (!z1 or z2 or ... or !zn)SAT は「a1 や zn などの変数にうまく true か false を代入して、上の式全体を true にできるか」という問題
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
3-SAT Faster and Simpler - Unique-SAT Bounds for PPSZ Hold in General