更新日時で差をつけろ

むしろ差をつけられている

Xmas Contest 2017 I - SAT Puzzle を z3 を使って解いた

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