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

#crystal #z3

Dominosa is a puzzle with simple rules:

there's a grid filled with numbers
you need to pair those numbers into dominos
each domino needs to be different

As usual, I recommend playing the puzzle a few times to get a good feel for it. It will make it easier to follow along.

I'll be using updated Crystal Z3 shard, as explained in the previous episode.

Plaintext input

Here's an example input:

77525629349
49071866039
82294832830
98723812246
50186000647
61556354899
56113420383
04114737281
06552340497
79171576958

Solver

#!/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

We're definitely taking advantage of Z3.add and of properly typed Model#[] here.

The nontrivial parts of the solver are add_domino method, and printing. With Z3 solvers it's fairly common that input and output are more complex than solver logic.

Arguably all the next if x == @xsize - 1 blocks could be replaced by some properly named helpers, hopefully it's not too complicated.

Result

$ ./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