前回「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
実行した結果は、以下の通り。
しかし、参考サイトとソースコードを比べると、僕のはとても汚い。
まず、同じ行に同じ数字が登場しない、というルールを表すのに、
ループを回すのに直値を使ってしまっているし、1行の中の4マスから任意に2マスを選択するところは、全組み合わせを手書きしてしまっている。
この部分は、参考サイトでは、
僕が知らなかった、transposeやcombinationといったメソッドを利用している。
transposeは、配列の行と列を転置するメソッドの様だ。
それから、combinationはその名の通り組み合わせを返してくれるらしい。
こういうメソッドを知っていると、配列のサイズが変更になったときにも対応できる美しいコードが書ける。
いや、知らなくても、こういうメソッド無いかな？って調べれば良かったんだ。
もし、調べてみても見つからなかったら、自分でメソッドを書いても良かったはずだ。
反省。
その他、zipやらflattenなどの、配列を上手く操作するメソッドを多様されていて、とても勉強になった。
さて、このように便利なSATソルバだが、半導体のフロアレイアウトの自動決定などに使われている、ということを最近知った。会員制の記事で恐縮だが、興味のある方は一読をおススメする。
それにしても、機械に自動的に問題を解かせる、ってのは男のロマンだな。久しぶりに、手を動かしながらワクワク感を覚えた。
$ 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ソルバだが、半導体のフロアレイアウトの自動決定などに使われている、ということを最近知った。会員制の記事で恐縮だが、興味のある方は一読をおススメする。
それにしても、機械に自動的に問題を解かせる、ってのは男のロマンだな。久しぶりに、手を動かしながらワクワク感を覚えた。
