Open Source Adventures: Episode 72: Crystal Z3 Solver for Dominosa Puzzle

77525629349
49071866039
82294832830
98723812246
50186000647
61556354899
56113420383
04114737281
06552340497
79171576958

#!/usr/bin/env crystal

require "z3"

class DominosaSolver
  @board : Array(Array(Int32))
  @xsize : Int32

  def initialize(path)
    @board = File.read_lines(path).map(&.chars.map(&.to_i))
    @ysize = @board.size
    @xsize = @board[0].size
    @solver = Z3::Solver.new
    @horizontal = {} of Tuple(Int32, Int32) => Z3::BoolExpr
    @vertical = {} of Tuple(Int32, Int32) => Z3::BoolExpr
    @dominos = {} of Tuple(Int32, Int32) => Array(Z3::BoolExpr)
  end

  def each_coord
    @xsize.times do |x|
      @ysize.times do |y|
        yield(x,y)
      end
    end
  end

  def connections(x,y)
    [
      @horizontal[{x,y}]?,
      @horizontal[{x-1,y}]?,
      @vertical[{x,y}]?,
      @vertical[{x,y-1}]?,
    ].compact
  end

  def add_domino(x1, y1, x2, y2, var)
    v1 = @board[y1][x1]
    v2 = @board[y2][x2]
    v1, v2 = [v1, v2].sort
    @dominos[{v1,v2}] ||= [] of Z3::BoolExpr
    @dominos[{v1,v2}].push var
  end

  def call
    # Setup horizontal variables
    each_coord do |x,y|
      next if x == @xsize - 1
      @horizontal[{x,y}] = var = Z3.bool("h #{x},#{y}")
      add_domino x, y, x+1, y, var
    end

    # Setup vertical variables
    each_coord do |x,y|
      next if y == @ysize - 1
      @vertical[{x,y}] = var = Z3.bool("v #{x},#{y}")
      add_domino x, y, x, y+1, var
    end

    # Each number belongs to exactly one domino
    each_coord do |x,y|
      @solver.assert 1 == Z3.add(connections(x,y).map{|v| v.ite(1,0)})
    end

    # Every type of domino has exactly one instance
    @dominos.each do |type, vars|
      @solver.assert 1 == Z3.add(vars.map{|v| v.ite(1,0)})
    end

    if @solver.satisfiable?
      model = @solver.model
      @ysize.times do |y|
        @xsize.times do |x|
          print @board[y][x]
          next if x == @xsize - 1
          print model[@horizontal[{x,y}]].to_b ? "*" : " "
        end
        print "\n"

        next if y == @ysize - 1

        @xsize.times do |x|
          print model[@vertical[{x,y}]].to_b ? "*" : " "
          next if x == @xsize - 1
          print " "
        end
        print "\n"
      end
    else
      puts "No solution"
    end
  end
end

DominosaSolver.new(ARGV[0]).call

$ ./dominosa 1.txt
7*7 5*2 5 6*2 9*3 4*9
        *
4 9 0 7 1 8 6*6 0 3 9
* * * *   *     * * *
8 2 2 9 4 8 3*2 8 3 0
        *
9 8*7 2 3 8*1 2*2 4 6
*     *           * *
5 0*1 8 6*0 0*0 6 4 7
                *
6*1 5*5 6*3 5*4 8 9*9

5 6 1 1*3 4*2 0*3 8*3
* * *
0 4 1 1*4 7*3 7*2 8 1
                  * *
0 6*5 5 2 3 4 0*4 9 7
*     * * * *
7 9*1 7 1 5 7 6*9 5*8