SMT solver 入門 - suer のブログ

SAT solver が周りでほのかに流行っている(いた?)ので，個人的には SAT solver よりも断然便利な SMT solver について書いてみようと思いたった．

SMT って?

SMT は Satisfiable Modulo Theories の略で，SAT だと命題変数を並べて CNF で記述しなければいけないところを，int とか，プログラムで使うような変数が扱える上，述語が使える．

なので一般に記述量が減り，人間に(SAT問題よりは)読みやすくなる傾向にあると思う．

SMT Solver

SMT Solver については http://combination.cs.uiowa.edu/smtlib/ でいろいろ見つかるけれど，ここでは The Yices SMT Solver を使ってみる．

環境準備

Mac OS X Leopard
Yices 4.2.2

例題

SAT ソルバで数独を解く方法 - まめめもの例をパクらせていただきました．

4x4の数独です．

4x4の数独の制約は，
1. 各マスは 1〜4のどれか
2. 同列に同数が現れない
3. 同行に同数が現れない
4. 同ブロックに同数が現れない

以下のように一部が埋められているとする．

記述

数独の制約をそのまま記述していく．

まず変数定義



;; 定義

(define x11::int)

(define x12::int)

(define x13::int)

(define x14::int)

(define x21::int)

(define x22::int)

(define x23::int)

(define x24::int)

(define x31::int)

(define x32::int)

(define x33::int)

(define x34::int)

(define x41::int)

(define x42::int)

(define x43::int)

(define x44::int)

define は変数定義だと思ってよい．

xmn で m行 n列のマスの値を表すことにする．

つまり以下のような感じ．



x11 x12|x13 x14

x21 x22|x23 x24




























-













x31 x32|x33 x34

x41 x42|x43 x44

ここから制約．

assert で制約式を追加．
assert の引数は述語．
で，述語はs式で書く．



;; (1) 各マスは 1 〜 4

(assert (and (<= 1 x11) (<= x11 4)))

(assert (and (<= 1 x12) (<= x12 4)))

(assert (and (<= 1 x13) (<= x13 4)))

(assert (and (<= 1 x14) (<= x14 4)))

(assert (and (<= 1 x21) (<= x21 4)))

(assert (and (<= 1 x22) (<= x22 4)))

(assert (and (<= 1 x23) (<= x23 4)))

(assert (and (<= 1 x24) (<= x24 4)))

(assert (and (<= 1 x31) (<= x31 4)))

(assert (and (<= 1 x32) (<= x32 4)))

(assert (and (<= 1 x33) (<= x33 4)))

(assert (and (<= 1 x34) (<= x34 4)))

(assert (and (<= 1 x41) (<= x41 4)))

(assert (and (<= 1 x42) (<= x42 4)))

(assert (and (<= 1 x43) (<= x43 4)))

(assert (and (<= 1 x44) (<= x44 4)))



;; (2) それぞれの列に重複は無い

(assert (and (/= x11 x21) (/= x11 x31) (/= x11 x41) (/= x21 x31) (/= x21 x41) (/= x31 x41)))

(assert (and (/= x12 x22) (/= x12 x32) (/= x12 x42) (/= x22 x32) (/= x22 x42) (/= x32 x42)))

(assert (and (/= x13 x23) (/= x13 x33) (/= x13 x43) (/= x23 x33) (/= x23 x43) (/= x33 x43)))

(assert (and (/= x14 x24) (/= x14 x34) (/= x14 x44) (/= x24 x34) (/= x24 x44) (/= x34 x44)))



;; (3) それぞれの行に重複は無い

(assert (and (/= x11 x12) (/= x11 x13) (/= x11 x14) (/= x12 x13) (/= x12 x14) (/= x13 x14)))

(assert (and (/= x21 x22) (/= x21 x23) (/= x21 x24) (/= x22 x23) (/= x22 x24) (/= x23 x24)))

(assert (and (/= x31 x32) (/= x31 x33) (/= x31 x34) (/= x32 x33) (/= x32 x34) (/= x33 x34)))

(assert (and (/= x41 x42) (/= x41 x43) (/= x41 x44) (/= x42 x43) (/= x42 x44) (/= x43 x44)))



;; (4) 同ブロックに同数が現れない

(assert (and (/= x11 x12) (/= x11 x21) (/= x11 x22) (/= x12 x21) (/= x12 x22) (/= x21 x22)))

(assert (and (/= x13 x14) (/= x13 x23) (/= x13 x24) (/= x14 x23) (/= x14 x24) (/= x23 x24)))

(assert (and (/= x31 x32) (/= x31 x41) (/= x31 x42) (/= x32 x41) (/= x32 x42) (/= x41 x42)))

(assert (and (/= x33 x34) (/= x33 x43) (/= x33 x44) (/= x34 x43) (/= x34 x44) (/= x43 x44)))



;; (5) すでに割り当てられているマス

(assert (= x14 4))

(assert (= x23 1))

(assert (= x24 2))

(assert (= x32 1))

(assert (= x33 4))

(assert (= x34 3))

(assert (= x41 4))

(assert (= x42 3))

(assert (= x43 2))

(assert (= x44 1))

最後におまじない



(set-evidence! true)

(check)

set-evidence! は evidence (充足するときの割り当て例) を表示するかどうかを指定する．
check を書くと，ここまでに追加されている制約の充足可能性を検査する．

実行

上記をこの順番のまま sudoku4x4.ys というファイルに保存し，下記のコマンドを発行．



 $ yices sudoku4x4.ys

下記の応答が返った．



sat

(= x11 1)

(= x12 2)

(= x13 3)

(= x14 4)

(= x21 3)

(= x22 4)

(= x23 1)

(= x24 2)

(= x31 2)

(= x32 1)

(= x33 4)

(= x34 3)

(= x41 4)

(= x42 3)

(= x43 2)

(= x44 1)

もとの表に割り当てるとこんな感じ．

とりあえず合ってそう．

まとめ

本当は配列とか自前述語とか使えばもっとスマートに書けるが，これでも CNF で書くよりは格段にみやすいのではないかと思う．
とくに Yices は C から叩ける API があったり，今回使ったもの以外にももっと沢山の便利な述語が使えたりするので非常に便利．
まだまだ奥が深いのでもっと勉強しなければ．