Solving Advent of Code Day 21 using Z3 and Ruby

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::IntExpr

You 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"
end

you 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!"
end

should print

$ ruby smm.rb
9567 + 1085 = 10652

Solving 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: 32

to 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_i

If 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.