VB.NETでも制約ソルバーを用いて数独を解きたい その1

はじめに

マイクロソフト・リサーチが開発しているz3定理証明器に興味を持ったのでそれについてです。

鶴亀算

まずはオンラインのコンソール鶴亀算解いてみましょう。

z3はSMT-LIB標準形式のバージョン2を解釈できるのでそれを用いて鶴亀算の各制約を記述します。 なお、SMT-LIBはS式で記述するみたいです。 LispSchemeを使ったことがある人ならおなじみでしょう。 おなじんでないひとは・・・がんばってください。

;; シンボルの定義
(declare-const kame Int)
(declare-const tsuru Int)
;; 制約を表現
(assert (= 8 (+ kame tsuru)))
(assert (= 26 (+ (* kame 4) (* tsuru 2))))
;; 検証
(check-sat)
;; 結果の取得
(get-model)
sat
(model 
  (define-fun tsuru () Int
    3)
  (define-fun kame () Int
    5)
)

数独

なんとなくで鶴亀算を解いたので、次はノリと勢いで数独を解いて行きましょう。

まずは各要素は1から9の間という制約を表現してみます。

(declare-const x_1_1 Int)
(assert (and (<= 1 x_1_1) (>= 9 x_1_1)))
(push)
;; ---------------------------
(assert (= x_1_1 1))
(check-sat)
;; ---------------------------
(pop)
(push)
;; ---------------------------
(assert (= x_1_1 9))
(check-sat)
;; ---------------------------
(pop)
(push)
;; ---------------------------
(assert (= x_1_1 10))
(check-sat)
;; ---------------------------

S式がなんとなくとっつきにくいかもしれませんが、やってるのは普通の条件式ですね。

sat
sat
unsat

ちなみに(pop)(push)はその時点でのコンテキストをスタックへプッシュ・ポップする命令です。 3行目の(push)だったら(declare-const x_1_1 Int)(assert (and (<= 0 x_1_1) (>= 9 x_1_1)))が評価された状態がスタックにプッシュされます。

次に各要素が異なるという制約を表現します。異なるという制約はdistinct演算子を使用します。

(declare-const x_1_1 Int)
(declare-const x_1_2 Int)
(declare-const x_1_3 Int)
(assert (distinct x_1_1 x_1_2 x_1_3))
(push)
;; ---------------------------
(assert (= x_1_1 1))
(assert (= x_1_2 2))
(assert (= x_1_3 3))
(check-sat)
;; ---------------------------
(pop)
(push)
;; ---------------------------
(assert (= x_1_1 1))
(assert (= x_1_2 2))
(assert (= x_1_3 1))
(check-sat)
sat
unsat

これで必要な制約をSMT-LIBで表現する準備が出来ました。 あとは心を無にしてひたすらエディタに放り込むだけです*1

問題はテキトーにヤフーで『数独 最高難易度』でググって出てきた結果を使用しています。

;; 01 02 03 | 04 05 06 | 07 08 09
;; 10 11 12 | 13 14 15 | 16 17 18
;; 19 20 21 | 22 23 24 | 25 26 27
;; ---------+----------+---------
;; 28 29 30 | 31 32 33 | 34 35 36
;; 37 38 39 | 40 41 42 | 43 44 45
;; 46 47 48 | 49 50 51 | 52 53 54
;; ---------+----------+---------
;; 55 56 57 | 58 59 60 | 61 62 63
;; 64 65 66 | 67 68 69 | 70 71 72
;; 73 74 75 | 76 77 78 | 79 80 81
;;
;; __ __ _5 | _3 __ __ | __ __ __
;; _8 __ __ | __ __ __ | __ _2 __
;; __ _7 __ | __ _1 __ | _5 __ __
;; ---------+----------+---------
;; _4 __ __ | __ __ _5 | _3 __ __
;; __ _1 __ | __ _7 __ | __ __ _6
;; __ __ _3 | _2 __ __ | __ _8 __
;; ---------+----------+---------
;; __ _6 __ | _5 __ __ | __ __ _9
;; __ __ _4 | __ __ __ | __ _3 __
;; __ __ __ | __ __ _9 | _7 __ __
;;
(declare-const x01 Int)
(declare-const x02 Int)
(declare-const x03 Int)
(declare-const x04 Int)
(declare-const x05 Int)
(declare-const x06 Int)
(declare-const x07 Int)
(declare-const x08 Int)
(declare-const x09 Int)
(declare-const x10 Int)
(declare-const x11 Int)
(declare-const x12 Int)
(declare-const x13 Int)
(declare-const x14 Int)
(declare-const x15 Int)
(declare-const x16 Int)
(declare-const x17 Int)
(declare-const x18 Int)
(declare-const x19 Int)
(declare-const x20 Int)
(declare-const x21 Int)
(declare-const x22 Int)
(declare-const x23 Int)
(declare-const x24 Int)
(declare-const x25 Int)
(declare-const x26 Int)
(declare-const x27 Int)
(declare-const x28 Int)
(declare-const x29 Int)
(declare-const x30 Int)
(declare-const x31 Int)
(declare-const x32 Int)
(declare-const x33 Int)
(declare-const x34 Int)
(declare-const x35 Int)
(declare-const x36 Int)
(declare-const x37 Int)
(declare-const x38 Int)
(declare-const x39 Int)
(declare-const x40 Int)
(declare-const x41 Int)
(declare-const x42 Int)
(declare-const x43 Int)
(declare-const x44 Int)
(declare-const x45 Int)
(declare-const x46 Int)
(declare-const x47 Int)
(declare-const x48 Int)
(declare-const x49 Int)
(declare-const x50 Int)
(declare-const x51 Int)
(declare-const x52 Int)
(declare-const x53 Int)
(declare-const x54 Int)
(declare-const x55 Int)
(declare-const x56 Int)
(declare-const x57 Int)
(declare-const x58 Int)
(declare-const x59 Int)
(declare-const x60 Int)
(declare-const x61 Int)
(declare-const x62 Int)
(declare-const x63 Int)
(declare-const x64 Int)
(declare-const x65 Int)
(declare-const x66 Int)
(declare-const x67 Int)
(declare-const x68 Int)
(declare-const x69 Int)
(declare-const x70 Int)
(declare-const x71 Int)
(declare-const x72 Int)
(declare-const x73 Int)
(declare-const x74 Int)
(declare-const x75 Int)
(declare-const x76 Int)
(declare-const x77 Int)
(declare-const x78 Int)
(declare-const x79 Int)
(declare-const x80 Int)
(declare-const x81 Int)
(assert (and (<= 1 x01) (>= 9 x01)))
(assert (and (<= 1 x02) (>= 9 x02)))
(assert (and (<= 1 x03) (>= 9 x03)))
(assert (and (<= 1 x04) (>= 9 x04)))
(assert (and (<= 1 x05) (>= 9 x05)))
(assert (and (<= 1 x06) (>= 9 x06)))
(assert (and (<= 1 x07) (>= 9 x07)))
(assert (and (<= 1 x08) (>= 9 x08)))
(assert (and (<= 1 x09) (>= 9 x09)))
(assert (and (<= 1 x10) (>= 9 x10)))
(assert (and (<= 1 x11) (>= 9 x11)))
(assert (and (<= 1 x12) (>= 9 x12)))
(assert (and (<= 1 x13) (>= 9 x13)))
(assert (and (<= 1 x14) (>= 9 x14)))
(assert (and (<= 1 x15) (>= 9 x15)))
(assert (and (<= 1 x16) (>= 9 x16)))
(assert (and (<= 1 x17) (>= 9 x17)))
(assert (and (<= 1 x18) (>= 9 x18)))
(assert (and (<= 1 x19) (>= 9 x19)))
(assert (and (<= 1 x20) (>= 9 x20)))
(assert (and (<= 1 x21) (>= 9 x21)))
(assert (and (<= 1 x22) (>= 9 x22)))
(assert (and (<= 1 x23) (>= 9 x23)))
(assert (and (<= 1 x24) (>= 9 x24)))
(assert (and (<= 1 x25) (>= 9 x25)))
(assert (and (<= 1 x26) (>= 9 x26)))
(assert (and (<= 1 x27) (>= 9 x27)))
(assert (and (<= 1 x28) (>= 9 x28)))
(assert (and (<= 1 x29) (>= 9 x29)))
(assert (and (<= 1 x30) (>= 9 x30)))
(assert (and (<= 1 x31) (>= 9 x31)))
(assert (and (<= 1 x32) (>= 9 x32)))
(assert (and (<= 1 x33) (>= 9 x33)))
(assert (and (<= 1 x34) (>= 9 x34)))
(assert (and (<= 1 x35) (>= 9 x35)))
(assert (and (<= 1 x36) (>= 9 x36)))
(assert (and (<= 1 x37) (>= 9 x37)))
(assert (and (<= 1 x38) (>= 9 x38)))
(assert (and (<= 1 x39) (>= 9 x39)))
(assert (and (<= 1 x40) (>= 9 x40)))
(assert (and (<= 1 x41) (>= 9 x41)))
(assert (and (<= 1 x42) (>= 9 x42)))
(assert (and (<= 1 x43) (>= 9 x43)))
(assert (and (<= 1 x44) (>= 9 x44)))
(assert (and (<= 1 x45) (>= 9 x45)))
(assert (and (<= 1 x46) (>= 9 x46)))
(assert (and (<= 1 x47) (>= 9 x47)))
(assert (and (<= 1 x48) (>= 9 x48)))
(assert (and (<= 1 x49) (>= 9 x49)))
(assert (and (<= 1 x50) (>= 9 x50)))
(assert (and (<= 1 x51) (>= 9 x51)))
(assert (and (<= 1 x52) (>= 9 x52)))
(assert (and (<= 1 x53) (>= 9 x53)))
(assert (and (<= 1 x54) (>= 9 x54)))
(assert (and (<= 1 x55) (>= 9 x55)))
(assert (and (<= 1 x56) (>= 9 x56)))
(assert (and (<= 1 x57) (>= 9 x57)))
(assert (and (<= 1 x58) (>= 9 x58)))
(assert (and (<= 1 x59) (>= 9 x59)))
(assert (and (<= 1 x60) (>= 9 x60)))
(assert (and (<= 1 x61) (>= 9 x61)))
(assert (and (<= 1 x62) (>= 9 x62)))
(assert (and (<= 1 x63) (>= 9 x63)))
(assert (and (<= 1 x64) (>= 9 x64)))
(assert (and (<= 1 x65) (>= 9 x65)))
(assert (and (<= 1 x66) (>= 9 x66)))
(assert (and (<= 1 x67) (>= 9 x67)))
(assert (and (<= 1 x68) (>= 9 x68)))
(assert (and (<= 1 x69) (>= 9 x69)))
(assert (and (<= 1 x70) (>= 9 x70)))
(assert (and (<= 1 x71) (>= 9 x71)))
(assert (and (<= 1 x72) (>= 9 x72)))
(assert (and (<= 1 x73) (>= 9 x73)))
(assert (and (<= 1 x74) (>= 9 x74)))
(assert (and (<= 1 x75) (>= 9 x75)))
(assert (and (<= 1 x76) (>= 9 x76)))
(assert (and (<= 1 x77) (>= 9 x77)))
(assert (and (<= 1 x78) (>= 9 x78)))
(assert (and (<= 1 x79) (>= 9 x79)))
(assert (and (<= 1 x80) (>= 9 x80)))
(assert (and (<= 1 x81) (>= 9 x81)))
(assert (distinct x01 x02 x03 x04 x05 x06 x07 x08 x09))
(assert (distinct x10 x11 x12 x13 x14 x15 x16 x17 x18))
(assert (distinct x19 x20 x21 x22 x23 x24 x25 x26 x27))
(assert (distinct x28 x29 x30 x31 x32 x33 x34 x35 x36))
(assert (distinct x37 x38 x39 x40 x41 x42 x43 x44 x45))
(assert (distinct x46 x47 x48 x49 x50 x51 x52 x53 x54))
(assert (distinct x55 x56 x57 x58 x59 x60 x61 x62 x63))
(assert (distinct x64 x65 x66 x67 x68 x69 x70 x71 x72))
(assert (distinct x73 x74 x75 x76 x77 x78 x79 x80 x81))
(assert (distinct x01 x10 x19 x28 x37 x46 x55 x64 x73))
(assert (distinct x02 x11 x20 x29 x38 x47 x56 x65 x74))
(assert (distinct x03 x12 x21 x30 x39 x48 x57 x66 x75))
(assert (distinct x04 x13 x22 x31 x40 x49 x58 x67 x76))
(assert (distinct x05 x14 x23 x32 x41 x50 x59 x68 x77))
(assert (distinct x06 x15 x24 x33 x42 x51 x60 x69 x78))
(assert (distinct x07 x16 x25 x34 x43 x52 x61 x70 x79))
(assert (distinct x08 x17 x26 x35 x44 x53 x62 x71 x80))
(assert (distinct x09 x18 x27 x36 x45 x54 x63 x72 x81))
(assert (distinct x01 x02 x03 x10 x11 x12 x19 x20 x21))
(assert (distinct x04 x05 x06 x13 x14 x15 x22 x23 x24))
(assert (distinct x07 x08 x09 x16 x17 x18 x25 x26 x27))
(assert (distinct x28 x29 x30 x37 x38 x39 x46 x47 x48))
(assert (distinct x31 x32 x33 x40 x41 x42 x49 x50 x51))
(assert (distinct x34 x35 x36 x43 x44 x45 x52 x53 x54))
(assert (distinct x55 x56 x57 x64 x65 x66 x73 x74 x75))
(assert (distinct x58 x59 x60 x67 x68 x69 x76 x77 x78))
(assert (distinct x61 x62 x63 x70 x71 x72 x79 x80 x81))
(assert (= x03 5))
(assert (= x04 3))
(assert (= x10 8))
(assert (= x17 2))
(assert (= x20 7))
(assert (= x23 1))
(assert (= x25 5))
(assert (= x28 4))
(assert (= x33 5))
(assert (= x34 3))
(assert (= x38 1))
(assert (= x41 7))
(assert (= x45 6))
(assert (= x48 3))
(assert (= x49 2))
(assert (= x53 8))
(assert (= x56 6))
(assert (= x58 5))
(assert (= x63 9))
(assert (= x66 4))
(assert (= x71 3))
(assert (= x78 9))
(assert (= x79 7))
(check-sat)
(get-model)
sat
(model 
  (define-fun x01 () Int
    1)
  (define-fun x75 () Int
    1)
  (define-fun x65 () Int
    8)
  (define-fun x24 () Int
    8)
  (define-fun x50 () Int
    9)
  (define-fun x59 () Int
    4)
  (define-fun x69 () Int
    1)
  (define-fun x21 () Int
    2)
  (define-fun x42 () Int
    3)
  (define-fun x44 () Int
    5)
  (define-fun x08 () Int
    9)
  (define-fun x55 () Int
    3)
  (define-fun x73 () Int
    5)
  (define-fun x19 () Int
    6)
  (define-fun x46 () Int
    7)
  (define-fun x15 () Int
    4)
  (define-fun x39 () Int
    8)
  (define-fun x72 () Int
    5)
  (define-fun x32 () Int
    8)
  (define-fun x37 () Int
    2)
  (define-fun x02 () Int
    4)
  (define-fun x47 () Int
    5)
  (define-fun x60 () Int
    2)
  (define-fun x68 () Int
    6)
  (define-fun x13 () Int
    6)
  (define-fun x16 () Int
    1)
  (define-fun x26 () Int
    4)
  (define-fun x80 () Int
    6)
  (define-fun x14 () Int
    5)
  (define-fun x54 () Int
    1)
  (define-fun x36 () Int
    2)
  (define-fun x31 () Int
    1)
  (define-fun x29 () Int
    9)
  (define-fun x43 () Int
    9)
  (define-fun x64 () Int
    9)
  (define-fun x06 () Int
    7)
  (define-fun x11 () Int
    3)
  (define-fun x05 () Int
    2)
  (define-fun x67 () Int
    7)
  (define-fun x76 () Int
    8)
  (define-fun x62 () Int
    1)
  (define-fun x09 () Int
    8)
  (define-fun x18 () Int
    7)
  (define-fun x30 () Int
    6)
  (define-fun x52 () Int
    4)
  (define-fun x12 () Int
    9)
  (define-fun x81 () Int
    4)
  (define-fun x27 () Int
    3)
  (define-fun x57 () Int
    7)
  (define-fun x51 () Int
    6)
  (define-fun x77 () Int
    3)
  (define-fun x07 () Int
    6)
  (define-fun x74 () Int
    2)
  (define-fun x40 () Int
    4)
  (define-fun x35 () Int
    7)
  (define-fun x61 () Int
    8)
  (define-fun x70 () Int
    2)
  (define-fun x22 () Int
    9)
  (define-fun x79 () Int
    7)
  (define-fun x78 () Int
    9)
  (define-fun x71 () Int
    3)
  (define-fun x66 () Int
    4)
  (define-fun x63 () Int
    9)
  (define-fun x58 () Int
    5)
  (define-fun x56 () Int
    6)
  (define-fun x53 () Int
    8)
  (define-fun x49 () Int
    2)
  (define-fun x48 () Int
    3)
  (define-fun x45 () Int
    6)
  (define-fun x41 () Int
    7)
  (define-fun x38 () Int
    1)
  (define-fun x34 () Int
    3)
  (define-fun x33 () Int
    5)
  (define-fun x28 () Int
    4)
  (define-fun x25 () Int
    5)
  (define-fun x23 () Int
    1)
  (define-fun x20 () Int
    7)
  (define-fun x17 () Int
    2)
  (define-fun x10 () Int
    8)
  (define-fun x04 () Int
    3)
  (define-fun x03 () Int
    5)
)

おわりに

やってみて思ったのですが、正直これを手入力するのはつらみポイントバクアゲなんてものではありません。 折れた心をセメントで塗り固めながら作業をしました。

定型的な制約を生成するのは手続き型と相性がよさそうです。つまり、制約の生成を手続き型にやらせて、解くのを制約ソルバーにやらせるのがよさそうです。 というわけで次回はVB.NETから制約を生成し、それをz3に放り込む方法を確認してみましょう。

*1:タイムアウトに引っかかったらごめんなさい