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
Story so far
Coming next
In the next episode I'll do one more puzzle solver, then it will be time to move on to different projects.
Top comments (0)