夜空日和 [出張版]

星を見上げながら、今日を語ってみようか

 

スポンサーサイト


Category: スポンサー広告   Tags: ---
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

(ほぼ) 全自動数独解答器


Category: 技術   Tags: ---
数独って、知ってますよね? → wikipedia

研究で SMT (Satisfiability Modulo Theories) を使うことになり、SMT-LIB (v2.0) 形式で数独を解いてみました。
( と言っても、既にやった人のブログそのままですが )



まず、馴染みが無い SMT (Satisfiability Modulo Theories) ですが。
簡単に書くと

「 cos(x) = sin(y) ∧ y > x2 となる実数 x, y の割り当てはあるか?」

って感じです。
実は、前身に SAT (Satisfiability problem:充足可能性問題) があります。
一般的に SAT は 2値(bool) しか使えないため、対象とする問題を変換する必要がありました。
これを「背景論理」という手段を入れて範囲に拡張したのが SMT です。 (・・・と認識しています)

さて、本題。

数独を SMT で解くってどうやるの?! って感じですが、ルール突っ込めば終わりです。
  • 変数 x を 9×9 = 81個用意する。
  • 変数は整数域(Int)で 1~9 までしか取れない条件を入れる。
  • 行、列、ブロック内で数字が重複しない条件を入れる。
  • 解く
これだけです。

詳細は、こちらのブログをお願いします。
どちらも、参考になります。

SMT solver は沢山ありますが、共通入力規格として SMT-LIB があります。
version が 1.2 と 2.0 の2つがあります。後者はまだ対応している物が少ないです。
でも、最新だから使っちゃいました。

(set-info :smt-lib-version 2.0)
(set-option :print-success false)
(set-option :produce-models true)
(set-logic QF_LIA)

; variables
(declare-fun x1_1 () Int)
 :
(declare-fun x9_9 () Int)

; 1 <= x <= 9
(assert (and (<= 1 x1_1) (<= x1_1 9)))
 :
(assert (and (<= 1 x9_9) (<= x9_9 9)))

; row constraints
(assert (distinct x1_1 x1_2 x1_3 x1_4 x1_5 x1_6 x1_7 x1_8 x1_9))
 :

; column constraints
(assert (distinct x1_1 x2_1 x3_1 x4_1 x5_1 x6_1 x7_1 x8_1 x9_1))
 :

; block constraints
(assert (distinct x1_1 x1_2 x1_3 x2_1 x2_2 x2_3 x3_1 x3_2 x3_3))
 :

; initial values
(assert (= x1_3 1))
 :

; execute
(check-sat)

; get values
(get-value (x1_1))
 :

; exit
(exit)
プログラムでは、Rubyで SMT solver (Z3) に直接流し込んでいます。
マシンと問題にもよりますが、3x3 は 1秒未満、 5x5 は 27919秒 (約8時間) でした。

約8時間で超難解な 5x5 が解けてしまうなんて、某ナンプレ雑誌も真っ青ですね。
しかも、どんな問題でも数式さえ立てられれば解くことは (理論上) 可能です。*1

こりゃ、強力ですね・・・

*1
どうやら、問題対象は 一階述語論理 みたいです。それ以上は無理ですね・・・

スポンサーサイト


Comments

Leave a Comment



10 2017
SUN MON TUE WED THU FRI SAT
1 2 3 4 5 6 7
8 9 10 11 12 13 14
15 16 17 18 19 20 21
22 23 24 25 26 27 28
29 30 31 - - - -

09

11


 
プロフィール

ひでたそ

Author:ひでたそ
Comment:
現役大学生で天文好き。
今日もどこかで、上を見ながら歩いています。

 
 
 
最新トラックバック
 
 
検索フォーム
 
 
 
ブロとも申請フォーム
 
QRコード
QRコード
 

Archive   RSS   Login

上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。