第10回資料
2018/07/18 通常回
z3とは?
SAT/SMTソルバ
複数の制約を満たすような値の組み合わせをいい感じに見つけてくれるソフトウェア
複数の制約=連立方程式, 「1つの行には1つの数字しか置けない」など
z3, minisatなど
sudo gem install z3
数独を解かせてみよう
code:solve.rb
require 'z3'
class Solver
def initialize
@solver = Z3::Solver.new
init_cells
end
def init_cells
@cells = (0...9).map do |x|
(0...9).map do |y|
end
end
@solver.assert @cells15 == 1 @solver.assert @cells17 == 8 @solver.assert @cells20 == 6 @solver.assert @cells21 == 4 @solver.assert @cells26 == 7 @solver.assert @cells35 == 3 @solver.assert @cells42 == 1 @solver.assert @cells43 == 8 @solver.assert @cells45 == 5 @solver.assert @cells50 == 9 @solver.assert @cells56 == 4 @solver.assert @cells58 == 2 @solver.assert @cells65 == 9 @solver.assert @cells66 == 3 @solver.assert @cells67 == 5 @solver.assert @cells70 == 7 @solver.assert @cells74 == 6 @solver.assert @cells84 == 2 end
def solve
(1..9).each do |x|
(1..9).each do |y|
@solver.assert @cellsxy >= 1 @solver.assert @cellsxy <= 9 end
end
@cells.each do |col|
@solver.assert Z3.Distinct(*col)
end
@cells.transpose.each do |row|
@solver.assert Z3.Distinct(*row)
end
@cells.each_slice(3) do |cols|
cols.transpose.each_slice(3) do |block|
@solver.assert Z3.Distinct(*block.flatten)
end
end
if @solver.satisfiable?
m = @solver.model
m.transpose.each do |line|
puts line.join(" ")
end
else
puts "Could not solve"
end
end
end
solver = Solver.new
solver.solve
ruby solve.rb