SATソルバのお試し（後編）

前回「SATソルバのお試し（前編）」の続きとして、SATソルバで何か例題を解いてみる。

検索すると、数独を例題としているサイトがあったので、それに倣ってみる。

実は、このサイトではruby-minisatを使って解いているので、ソースコードそのまんまでも動く。
でも、それでは学習にならないので、解説だけは参考にしながら独自に実装。
後述するが、このコードは汚いので、追試する人は先ほど紹介した参考サイトを見たほうが良いだろう。

#
# * 2 | * 4
# 1 * | * *
# ---+---
# * * | 3 *
# * * | * *
#

require "minisat"
solver = MiniSat::Solver.new

arr =
  (0...4).map do
    (0...4).map do
      (0...4).map { solver.new_var }
    end
  end

arr.each do |row|
  row.each do |square|
    solver << square
  end
end

for k in 0...4 do
  for j in 0...4 do
    solver << [-arr[0][j][k], -arr[1][j][k]]
    solver << [-arr[0][j][k], -arr[2][j][k]]
    solver << [-arr[0][j][k], -arr[3][j][k]]
    solver << [-arr[1][j][k], -arr[2][j][k]]
    solver << [-arr[1][j][k], -arr[3][j][k]]
    solver << [-arr[2][j][k], -arr[3][j][k]]
  end
end

for k in 0...4 do
  for i in 0...4 do
    solver << [-arr[i][0][k], -arr[i][1][k]]
    solver << [-arr[i][0][k], -arr[i][2][k]]
    solver << [-arr[i][0][k], -arr[i][3][k]]
    solver << [-arr[i][1][k], -arr[i][2][k]]
    solver << [-arr[i][1][k], -arr[i][3][k]]
    solver << [-arr[i][2][k], -arr[i][3][k]]
  end
end

solver << arr[0][1][1]
solver << arr[0][3][3]
solver << arr[1][0][0]
solver << arr[2][2][2]

solver.solve

ans =
  arr.map do |row|
    row.map do |square|
      (1..4).find do |i|
        solver[square[i - 1]]
      end
    end
  end

ans.each do |row|
  puts row.join(" ")
end

実行した結果は、以下の通り。

$ ruby sudoku.rb
3 2 1 4
1 4 2 3
4 1 3 2
2 3 4 1
$

どうやら正しい結果が出てるっぽい。
しかし、参考サイトとソースコードを比べると、僕のはとても汚い。

まず、同じ行に同じ数字が登場しない、というルールを表すのに、

for k in 0...4 do
  for j in 0...4 do
    solver << [-arr[0][j][k], -arr[1][j][k]]
    solver << [-arr[0][j][k], -arr[2][j][k]]
    solver << [-arr[0][j][k], -arr[3][j][k]]
    solver << [-arr[1][j][k], -arr[2][j][k]]
    solver << [-arr[1][j][k], -arr[3][j][k]]
    solver << [-arr[2][j][k], -arr[3][j][k]]
  end
end

とやってしまっている所が良くない。
ループを回すのに直値を使ってしまっているし、1行の中の4マスから任意に2マスを選択するところは、全組み合わせを手書きしてしまっている。

この部分は、参考サイトでは、

# 各行に同じ数字が 2 回以上現れない
field.each do |row|
  row.transpose.each do |vars|
    vars.combination(2) do |x, y|
      solver << [-x, -y]
    end
  end
end

となっており美しい。

僕が知らなかった、transposeやcombinationといったメソッドを利用している。
transposeは、配列の行と列を転置するメソッドの様だ。
それから、combinationはその名の通り組み合わせを返してくれるらしい。
こういうメソッドを知っていると、配列のサイズが変更になったときにも対応できる美しいコードが書ける。
いや、知らなくても、こういうメソッド無いかな？って調べれば良かったんだ。
もし、調べてみても見つからなかったら、自分でメソッドを書いても良かったはずだ。
反省。
その他、zipやらflattenなどの、配列を上手く操作するメソッドを多様されていて、とても勉強になった。

さて、このように便利なSATソルバだが、半導体のフロアレイアウトの自動決定などに使われている、ということを最近知った。会員制の記事で恐縮だが、興味のある方は一読をおススメする。

それにしても、機械に自動的に問題を解かせる、ってのは男のロマンだな。久しぶりに、手を動かしながらワクワク感を覚えた。