20行ちょっとで高速な数独ソルバーとPropLogic

Rubyで数独ソルバーを作ってみましたが、ささっと作っただけですぐ解けるものができました。

作っていたGem

先日からPropLogicというGemを作っていました。これはどういうことに使おうと思って作ったのかというと、いろんな問題を解く上でSATソルバーが便利だったのですが、いちいちCNFを考えたり、変換コードを書くのも面倒になってきたので、そのあたりを自動化して、ついでにRubyの演算子オーバーロードを使ってa | (b & ~c)のように書ければ便利だなと思って、Gemにしてみました。

解き方の方針

というわけで、「方針」なんてものはなくて、ただSATソルバー任せにするだけです。幸い、数独の場合は81マス×数字9つに対応する729本の変数を立てて、

• どのマスにも数字が1つずつ入る
• 縦の列の中で同じ数字が1つずつ入る
• 横の行の中で同じ数字が1つずつ入る
• 3*3のブロックの中で同じ数字が1つずつ入る
• もともと入っている数字については、そのまま条件にする

このようにすんなり条件化できます。

作ってみた数独ソルバー

require 'prop_logic/minisat'

# 初期盤面を入れておく
arr = [
 [0, 0, 0, 0, 0, 0, 0, 0, 0],
 [0, 0, 0, 0, 0, 0, 0, 0, 0],
 [0, 0, 0, 0, 0, 0, 0, 0, 0],
 [0, 0, 0, 0, 0, 0, 0, 0, 0],
 [0, 0, 0, 0, 0, 0, 0, 0, 0],
 [0, 0, 0, 0, 0, 0, 0, 0, 0],
 [0, 0, 0, 0, 0, 0, 0, 0, 0],
 [0, 0, 0, 0, 0, 0, 0, 0, 0],
 [0, 0, 0, 0, 0, 0, 0, 0, 0]
]

conds=[]
vars=(0..728).map{PropLogic.new_variable}
81.times do |i|
  # 最初からの数字
  conds << vars[i*9+arr[i/9][i%9]-1] if arr[i/9][i%9] != 0
  # 各マスに1つ以上数字が入る
  conds << PropLogic.all_or(*(0..8).map{|j| vars[i*9+j]})
  [*0..8].combination(2) do |a,b|
    # 同じマスの数字は1つ以下
    conds << (~vars[i*9+a]|~vars[i*9+b])
    # 行に同じ数字は1つ以下
    conds << (~vars[(u=i/9)*81+a*9+(d=i%9)]|~vars[(i/9)*81+b*9+i%9])
    # 列に同じ数字は1つ以下
    conds << (~vars[a*81+i]|~vars[b*81+i])
    # ブロックに同じ数字は1つ以下
    conds << (~vars[(u/3)*243+(a/3)*81+(u%3)*27+(a%3)*9+d]|~vars[(u/3)*243+(b/3)*81+(u%3)*27+(b%3)*9+d])
  end
end
# SATソルバーを実行
sat=(expr=PropLogic.all_and(*conds)).sat?
if sat
  # trueのものだけ抽出して、元のところに書き戻し
  sat.terms.select{|t| t.is_a?(PropLogic::Variable)}.each do |v|
    num = vars.index(v)
    arr[num/81][(num/9)%9] = num % 9 +1
  end
  # 別解チェック
  puts 'unique' if (expr & ~sat).unsat?
  arr.each{|row| puts row * '|'}
else
  puts 'not found'
end

行を削るために3重ループにすべきところを1つのループで回して、変数の桁ごとに意味を分けているので少々読みづらいですが、これだけのコードで世界一難しい数独も数秒で一意解を確認できました。

PropLogicの使い方

ReadMeにも書いたのですが、PropLogic標準のSATソルバーは全探索するというデバッグ用のもので、実用性能が出ません。ということで、ruby-minisatを呼ぶ形にしたprop_logic-minisatをrequireしています。

そして、基本的にはPropLogic.new_variableで変数を宣言して、あとはそれらの変数をNOT（~、-@）、AND（&）、OR（|）して条件を組み立てていきます。そして最後にsat?とすると、その条件式がSATソルバーに投げられて、充足可能であれば充足するように与えた変数とその否定をANDしたものが、充足不能ならfalseが返ってきます。

もっとも、この数独程度であれば、ruby-minisatを直接使ってもそこまで面倒なことにはなりません。