Posted on Jul 10, 2022

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