This year (2022) I decided to finally try to use Z3 to solve an Advent Of Code challenge, Day 21, to be precise.
Z3 is a theorem prover/SAT/SMT solver, which means “it will solve problems for you“. This is what computers are supposed to do, and I loved this stuff since I did an Operational Research exam in University.
Z3 can solve a variety of problems, but for this problem we just need to understand how it solves simple equations.
How to do algebra with Z3/Ruby
The Ruby bindings for Z3 are not as popular as, say, the python ones, but they work just fine. Install Z3 using your favorite tool (mine is MacPorts), and then the gem
$ port install z3
... compiling stuff
$ gem install z3
... compiling more stuff
$ ruby -r z3 -e 'p Z3.class'
Module
You can start coding now.
To solve an equation with Z3 you define a model composed of variables, values, and constraints, and then ask the solver to fill in the blanks.
The simplest thing you can do is a basic math expression
require 'z3'
solver = Z3::Solver.new
# the argument is the name of the variable in the model
a = Z3.Int('a')
b = Z3.Int('b')
x = Z3.Int('x')
solver.assert a == 1
solver.assert b == 3
solver.assert x == a + b
if solver.satisfiable?
p solver.model
else
puts "I can't solve that, Dave"
end
running this should give you
$ ruby additionz3.rb
Z3::Model<a=1, b=3, x=4>Behold! You can do basic math!
The interesting bit is that Z3.Int is a Z3::IntExpr object, and when you mix it with numbers or other expressions you get back more of the same, you can explore this in irb
>> require 'z3'
=> true
>> a = Z3.Int('a')
=> Int<a>
>> a.class
=> Z3::IntExpr
>> b = a+1
=> Int<a + 1>
>> b.class
=> Z3::IntExprYou can of course use other operators, such as relational operators. This is how you solve the problem of finding a number between two others
require 'z3'
solver = Z3::Solver.new
a = Z3.Int('a')
b = Z3.Int('b')
x = Z3.Int('x')
solver.assert a == 1
solver.assert b == 3
solver.assert x > a
solver.assert x < b
if solver.satisfiable?
p solver.model # Z3::Model<a=1, b=3, x=2>
else
puts "I can't do that Dave"
endyou can solve a system of equations in pretty much the same way. The classic puzzle SEND+MORE=MONEY where each letter is a different digit can be solved like this
require "z3"
solver = Z3::Solver.new
variables = "sendmoremoney".chars.uniq.each_with_object({}) do |digit, hash|
# All variables are digits
var = Z3.Int(digit)
solver.assert var >= 0
solver.assert var <= 9
hash[digit] = var
end
# define the words in terms of the digits
send = variables["s"] * 1000 + variables["e"] * 100 + variables["n"] * 10 + variables["d"]
more = variables["m"] * 1000 + variables["o"] * 100 + variables["r"] * 10 + variables["e"]
money = variables["m"] * 10000 + variables["o"] * 1000 + variables["n"] * 100 + variables["e"] * 10 + variables["y"]
# the leftmost digit is never zero
solver.assert variables['s'] > 0
solver.assert variables['m'] > 0
# all digits are different
solver.assert Z3.Distinct(*variables.values)
# define the actual expression
solver.assert money == send + more
if solver.satisfiable?
# get the values from the model, indexed by their name
values = solver.model.to_h
# map each letter to the variable and find each variable in the model
"send + more = money".chars.map do |char|
var = variables[char]
print values[var] || char
end
puts
else
p "Impossibru!"
endshould print
$ ruby smm.rb
9567 + 1085 = 10652Solving Day 21 with Z3
Spoiler alert: this covers part 2 which is not visible unless you solve part 1.
The problem is: you have a set of monkeys shouting at each other, defined like this:
root: pppw = sjmn
dbpl: 5
cczh: sllz + lgvd
zczc: 2
ptdq: humn - dvpt
dvpt: 3
lfqf: 4
humn: ?
ljgn: 2
sjmn: drzm * dbpl
sllz: 4
pppw: cczh / lfqf
lgvd: ljgn * ptdq
drzm: hmdt - zczc
hmdt: 32to the left of the : you have the monkey name, and to the right something they shout. A monkey shouts either a number, or the result of an operation based on numbers shouted by other monkeys, except for two of them: the monkey named root will check if the two numbers are equal, and humn represents you: you need to yell the right number so the equality check returns true.
My Clever Reader will have realized this is a simple algebraic problem, but the real input is large, to solve it you would have to think, determine the order of the operations, build a tree.. yeah I got bored already.
But executing instructions is what the Ruby interpreter does. And there is a clear mapping from the input a ruby+z3 instruction. So… let’s just transpile the input to a ruby program!
Each input line becomes an assert, we add a prologue, eval it, and then ask for a solution:
require 'z3'
input = <<~INPUT.lines
root: pppw + sjmn
dbpl: 5
cczh: sllz + lgvd
zczc: 2
ptdq: humn - dvpt
dvpt: 3
lfqf: 4
humn: 5
ljgn: 2
sjmn: drzm * dbpl
sllz: 4
pppw: cczh / lfqf
lgvd: ljgn * ptdq
drzm: hmdt - zczc
hmdt: 32
INPUT
# create a hash monkey-name -> variable
# so we can look them up by name
env = Hash.new { |h, k| h[k] = Z3.Int(k) }
# convert the input to a ruby program
prog = input.map do |l|
# root checks equality
l = l.sub(/root: (.*) \+ (.*)\n/, 'solver.assert env["\1"] == env["\2"]' + "\n")
# this is our incognita, just get rid of it
l = l.sub(/humn: (.*)\n/, "\n")
# assert a variable as an exact number
l = l.sub(/(\w+): (\d+)\n/, 'solver.assert(env["\1"] == \2)' + "\n")
# assert a variable as the result of a binary operation
l = l.sub(/(\w+): (\w+) (.) (\w+)\n/, 'solver.assert(env["\1"] == (env["\2"] \3 env["\4"]))' + "\n")
l
end
solver = Z3::Solver.new
# ger the program in here
eval(prog.join)
# solve and show our solution
p solver.satisfiable?
# ask for a solution
p solver.model.to_h[env["humn"]].to_iIf you remove the input, this boils down to ~10 lines of code.
Is it ugly? Yes. Is it cheating? Probably. Is it running eval on random input I just downloaded from the internet? You bet it is.
But I had a lot of fun.
