Xmas Contest 2017のI - SAT Puzzleのパズルをz3というSMTソルバを使って解いてみた。
あとでminisatが解釈できるDIMACS CNFを出力するようにして実際にジャッジにも出してみたい。
参考にしたのはここ。
Xmas Contest 2017 I問題 SAT Puzzle 解説
SAT ソルバー 入門 JOI春合宿のスライド。
パズルをSugar制約ソルバーで解く
z3は単なるソルバなので、そのソルバを使う言語は自由に選べる。z3 gemがあったのでRubyで書いた。
隣接の判定を8方向で行ってたりいろいろ間違えたりして5時間ぐらいかかった…
exampleを見てなんとなくで書いているのでもっとスマートに書けるかも。
require 'z3' class PuzzleSolver def initialize board @board = board @data = [] @constraints = [] @solver = Z3::Solver.new end def solve @data = (0...6).map do |y| (0...6).map do |x| make_cell x, y, @board[y][x] end end 6.times do |y| 6.times do |x| make_constraints_connectivity x, y end end make_constraints_unique if @solver.satisfiable? m = @solver.model @data.each do |row| puts row.map {|k| m[k[:c]].to_i == 1 ? 'x' : '.' }.join end else puts 'could not solve' end end def make_cell x, y, isblack c = Z3.Int "cell(#{x}, #{y})" g = [] 4.times do |i| g[i] = Z3.Int "group#{i}(#{x}, #{y})" @solver.assert 0 <= g[i] @solver.assert g[i] <= 4 end @solver.assert Z3.Or(c == 0, c == 1) @solver.assert c == 1 if isblack # c, g1~g4から1つ以上が真で、2つ以上は同時に真にならない => ちょうど一つが真 @solver.assert Z3.Or(g[0] > 0, g[1] > 0, g[2] > 0, g[3] > 0, c == 1) [c, *g].combination(2) do |a, b| @solver.assert Z3.Or(a == 0, b == 0) end {c: c, g: g} end def make_constraints_unique 4.times do |group| # for group0, 1, 2, 3 group_ints = @data.map do |row| row.map { |d| d[:g][group] } end.flatten 1.upto(4) do |node_num| # group_intsのどれかがそれぞれノード番号1,2,3,4になる @solver.assert Z3.Or(*group_ints.map { |gi| gi == node_num }) group_ints.combination(2) do |a, b| @solver.assert Z3.Or(a != node_num, b != node_num) end end end end def make_constraints_connectivity x, y 4.times do |group| g = @data[y][x][:g][group] # 連結(ノード番号1を根とする有向木のように考えて、ノードの番号が2以上のときは自分より小さい番号のノートを隣に置く) r = adjacent(x, y).map do |nx, ny| Z3.And(@data[ny][nx][:g][group] > 0, @data[ny][nx][:g][group] < g) end @solver.assert Z3.Implies(g > 1, Z3.Or(*r)) # 異なるグループのマスが隣接しない r = adjacent(x, y).map do |nx, ny| ([0, 1, 2, 3] - [group]).map { |other_group| @data[ny][nx][:g][other_group] == 0 } end @solver.assert Z3.Implies(g > 0, Z3.And(*r.flatten)) # r = adjacent(x, y).map do |nx, ny| # @data[ny][nx][:g4] > g4 # end # @solver.assert Z3.Implies(g4 > 0, Z3.Or(*r)) # g4 == 4 のときに不可能 end end def adjacent x, y r = [] r << [x-1, y ] if x > 0 r << [x , y-1] if y > 0 r << [x , y+1] if y < 5 r << [x+1, y ] if x < 5 r end end board = ' ...... ...x.. ..x..x x..x.. ....xx x.x..x ' board = board.split(' ').map { |line| line.chars.map { |ch| ch == 'x' } } solver = PuzzleSolver.new board solver.solve
$ ruby solve_by_z3.rb x...x. .x.x.. ..xx.x x.xxxx xx..xx xxx..x