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.

Advent of Code 2021: Day 6

I’ve been a bit busy so I skipped doing the tasks in Raku for a couple days, but today’s seemed fun. As usual SPOILERS ahead.

So the problem is basically: you have certain amounts of fish which have a “spawn-timer”, when they reach it they get reset to 6, and create a new fish with a spawn timer set at 8. Given an initial list of fish, we want to know how many fish we have after some days.

You, Clever Reader will certainly have noticed that we have an exponential behaviour: at each step we generate more fish, which will generate more more fish next time, and more more more fish and so on§.

The abstract solution in my mind would be:

  • set the initial values in some container structure
  • call some step function the given amount of days
  • count the total entries in the container

This, more or less

sub solve(@ints, $days) { # ints is something like [1, 2, 3, 3, 1, 4..]
  <whatever>
  step(<whatever>) for ^$days;
  [+] <whatever>;
}

the only interesting thing here is the construct

<do-something> for ^$number

where ^$number is a short form to define a range from 0 to $number and the rest is a short form to do a loop over the right hand size of the for keyword.

Extended this might look like

for 0..$days -> $day { <do-something> }

which I find less entertaining§.

The question to answer next is: what should we use as container?

Raku obviously has a Hash class, and we could initialize it with a default and then iterate over the initial values to build.

> my @ints= [1, 3, 3, 3, 3, 2]
[1 3 3 3 3 2]
> my %counts is default(0);
{}
> %counts{$_}++ for @ints
Nil
> %counts
{1 => 1, 2 => 1, 3 => 4}

The only new bit we see is the is default annotation that builds a container with a default value. But it seemed weird I have to do this, surely Raku has some builtin way to count things, like Ruby’s Enumerable#tally ?

And of course it does. It has More Than One Way To Do It, of course. For example, it provides a Bag class which is an immutable container for counting items, and can be extracted from another sequence trivially

> my @ints = [1, 3, 3, 3, 3, 2]
[1 3 3 3 3 2]
> @ints.Bag
Bag(1 2 3(4))

And a corresponding BagHash which returns a mutable container for counting.

Being a map from Any to Int these also come with a nice default, so when we access a missing item we get 0

> my $bh = @ints.BagHash
BagHash(1 2 3(4))
> $bh{1}
1
> $bh{2}
1
> $bh{3}
4
> $bh{99}
0

Wait, you might say, why are you using a scalar for that object, instead of a hash? Shouldn’t it be %bh rather than $bh?

The answer is: I don’t really know§

> my %bh-as-hash = $bh
{1 => 1, 2 => 1, 3 => 4}
> %bh-as-hash{99}  # no default in the hash!
(Any)
> $bh{99}          # still default in the BagHash!
0
> $bh{99} = 3      # you can update the BagHash
3
> $bh{99}
3
> %bh-as-hash{99}  # but the hash is unaffected
(Any)

You can alternatively use the := binding operator, which performs an assignment without casting:

> my %bh-as-hash-casted := $bh  # notice the representation
BagHash(1 2 3(4) 99(3))
> %bh-as-hash-casted{100} = 100 # it's the same object!
100
> $bh{100}
100

So our full solve can be

sub solve(@ints, $days) {
  my $counts = @ints.BagHash;
  step($counts) for ^$days;
  [+] $counts.values;
}

Now, how does the step function look? It is pretty straightforward, but it has a tricky bit

sub step($counts) {
  my $old = $counts.clone;
  for 8...0 -> $idx {
    $counts{$idx} = $old{$idx + 1};
    if $idx == 0 {
      $counts{8} = $old{0};
      $counts{6} += $old{0};
    }
  }
}

Do you see the… oddity? Look at this:

> for 1..3 -> $i { say $i }
1
2
3
> for 1...3 -> $i { say $i }
1
2
3
> for 3..1 -> $i { say $i }
Nil
> for 3...1 -> $i { say $i }
3
2
1

you cannot iterate in reverse one of those! This is because the .. operator builds a Range while ... builds a Seq. A Range is list of consecutive numbers, with a beginning and an end, while a Seq is something that can be iterated over.

So there are no numbers in an inverse Range, and if you iterate over it you get zero iterations. In my very humble rubyist opinion, this is very confusing™ , but I guess real Raku people are used to it.

Back to our task: of course, the Astute Reader will have noticed we can do this more tersely by simply shifting the array and adding it to itself, and then brining back the extra items. This is a simpler solution, and it’s pretty nice, but we need to build a list rather than a BagHash:.

sub solve2(@ints, $days) {
  my @list is default(0);      # create a list with default value 0
  @list[$_]++ for @ints;       # add all the fish to it
  step2(@list) for ^$days;     # do the steps
  [+] @list;                   # add up the values in the list
}

I have a feeling the first two lines can be collapsed, but I don’t know how, if you have an idea please let me know in the comments.

Our step function becomes very small

sub step2(@counts) {
  @counts.rotate;
  @counts[6] += @counts[8];
}

And honestly, I feel this is as expressive as it can be.

See you next time!

Advent of Code 2021: Day 2

Hello again!

So, Day 2 is not a particularly interesting problem: basically we have a stream of commands, and we need to move a submarine correspondingly, then in the last step we need to compute the product of the depth and horizontal distance

For problem 2, we are going to have “up N”, “down N” and “forward N”, which will respectively affect the aim of the submarine and the position.

This would be pretty trivial to do with a loop and a case/switch statement (which in Raku is called given/when) but I think it’s a cool chance to try out Raku’s multimethods.

A class definition in Raku looks like this

class Sub {
  has $.aim = 0;
  has $.depth = 0;
  has $.horizontal = 0;
  method process($operation, $num) { ... }
}

The $. is a twigil which says “this is a scalar value and it’s private but has accessor methods“.§

Methods (and Routines in general) support multiple dispatch which can happen through class, traits, or any specific attribute of the parameter (see the Signature class). In our case, we want to dispatch through the operation name, so we can do this§

multi method process("forward", $num) {
  ...
}
multi method process("up", $num) {
  ...
}
multi method process("down", $num) {
  ...
}

The actual implementation would be: when we go “up” or “down, we want to alter the aim, and when we go “forward” we move by the given amount horizontally, and by aim * num vertically.

We could alter the values in the given clasinstance, but… it’s uglier! The declared instance variables are immutable, if we want them to be mutable we should have used the rw trait, like this

class Sub {
  has $.aim = 0 is rw;
  has $.depth = 0 is rw;
  has $.horizontal = 0 is rw;
}

Raku is pushing gently against us so we prefer immutability, and who am I to go against that?

EDIT: as noted by mscha in the comments, this is incorrect. The variables are mutable, we could always assign them from within the instance, referring to them with the $! twigil, e.g. $!aim += $num. The is rw only refers to generating setter methods so they’re accessible from outside. Sorry, I’m still learning.

So, each of our process() calls will instead produce a new object by adjusting the current one. Luckily, the language has a pretty nice functionality to help with that: the clone() method accepts an argument to tweak the cloned object, so our code would look like this

class Sub {
  has $.aim = 0;
  has $.depth = 0;
  has $.horizontal = 0;

  multi method process("forward", $num) {
    self.clone(horizontal => $.horizontal + $num, depth => $.depth + $num * $.aim)
  }
  multi method process("up", $num) {
    self.clone(aim => $.aim - $num)
  }
  multi method process("down", $num) {
    self.clone(aim => $.aim + $num)
  }
}

This looks pretty nice to me! Now we only need to plug this into processing the commands. But I thought, well, we decided to be immutable, right? So let’s do this with reduce.

Rather than use the reduce metaoperator like last time, we can use the actual reduce routine. It works similar to other similar function in Python/Ruby/JavaScript/whatever.

my @words = 'day2.txt'.IO.words; # read all words
my @pairs = @words.rotor(2); # pair them up
my $sub = Sub.new # get a sub
<something with $sub and @pairs>.reduce(<block>) # iterate on values

The problem, is that, from what I understand, we cannot pass an initial value (our $sub) as an argument. The way to handle that is through using a Slip.

A Slip allows us to treat a list “as if it was typed there”. For example we can use it to prepend items to a list

> my @list = 1,2,3
[1 2 3]
> my @list2 = 3, @list
[3 [1 2 3]]
> my @list2 = 3, |@list
[3 1 2 3]

Or to use a list as an argument to a multi-argument routine

> my @pair = 1,2
[1 2]
> sub f($a, $b) { say "a: $a, b $b" }
&f
> f @pair
Too few positionals passed; expected 2 arguments but got 1
  in sub f at <unknown file> line 1
  in block <unit> at <unknown file> line 1

> f |@pair
a: 1, b 2

This is akin to the concept of “splat” in ruby, tho it’s somewhat more formalized.

So, we can pass an initial value to reduce by simply prepending it to the commands array:

($sub, |@pairs).reduce(<something>)

something should be a routine that takes two arguments (the accumulator and the next element) and returns a new value for the accumulator. This means it will call process(), and we can once again use a Slip!

($sub, |@pairs).reduce({ $^a.process(|$^b) })

Notice the $^ sourcery: in Raku you can use the ^ twigil to access variables implicitly, they will just be assigned from the arguments in order of definition. This call is effectively equivalent to

($sub, |@pairs).reduce(-> $a, $b { $a.process($b[0], $b[1]) } )

Now we just have to add a method to compute the final value, which is depth * horizontal, and putting all together we get

class Sub {
  has $.aim = 0;
  has $.depth = 0;
  has $.horizontal = 0;

  multi method process("forward", $num) {
    self.clone(horizontal => $.horizontal + $num, depth => $.depth + $num * $.aim)
  }

  multi method process("up", $num) {
    self.clone(aim => $.aim - $num)
  }

  multi method process("down", $num) {
    self.clone(aim => $.aim + $num)
  }

  method value {
    $.horizontal * $.depth
  }

}

my @words = '2.txt'.IO.words;

say (Sub.new, |@words.rotor(2)).reduce({ $^a.process(|$^b) }).value

which I find somewhat nice. I have to say, I still don’t like twigils, and I think I’m missing some way to write objects more tersely, if you know Raku better than me please let me know in the comments.

See you next time, happy hacking!

Advent of Code 2021: Day 1

Oh oh oh! Finally it’s that time of the year again!

I love Advent of Code and I’ve played it with friends and colleagues for years. Usually, I try to solve it in Ruby, since I’m very familiar with it, and so the effort is only on task solving rather than on learning the language and tooling.

But this year, I thought I might do it both in Ruby and in Raku (The Language Formerly Known As Perl 6), by first solving it in Ruby, and then if I have time trying to solve it again in Raku.

So, here’s a quick view of a couple solutions to the problems in Day 1. Stick to the end for the cool solution past the initial line noise 🙂

SPOILERS AHEAD

The first problem is basically: given a list of values, count the number of times they increase

In Ruby 3, this could look like this

def solve1(array)
  array.                # [1, 2, 5, 4]
    .each_cons(2).      # [(1, 2), (2, 5), (5, 4)]
    .count { _1 < _2 }. # 2
end

AKA: get a sliding window of pairs from the initial array, then count the occurrences where the first value in the pair is less than the second value in the pair. Notice the fancy anonymous positional block arguments!

You can do more or less the same in Raku, but I’m not aware of a .count method that takes a block§, but well, we can still do this in three steps:

  • build the sliding window
  • select the items matching the condition
  • get the size of the filtered list

Raku does not have each_slice, instead it has a .rotor method which is a generalization of “iterate and group“, you can define in one go both the size of the group and the offset, i.e.

> my @ints = [1, 2, 3, 4, 5, 6, 7, 8, 9]
[1 2 3 4 5 6 7 8 9]
> @ints.rotor(2)  # group by 2 
((1 2) (3 4) (5 6) (7 8))
> @ints.rotor(2 => 1)  # group by 2, and move by one after 
((1 2) (4 5) (7 8))
> @ints.rotor(2 => -1)  # group by 2, and move back by one after 
((1 2) (2 3) (3 4) (4 5) (5 6) (6 7) (7 8) (8 9))

The actual signature of this method is even more flexible, but this should be enough for us.

To filter we can use .grep, which takes a block. We can do this javacript-like, passing a block with a pointed arrow.§

Then we get the size of the list, which is done with prefix '+' . This is an odd perlism, just accept it.

+ @ints.rotor(2 => -1).grep(-> ($a, $b) { $a < $b })

So, that should work. But at this point it’s just un uglier Ruby! We can do better!

To get there, let’s first see a different way we can build the list of pairs: we can slice the list and merge it with itself, an operation which most languages call zip.

Raku also calls it zip, but it has something cooler than a function: it has a zip metaoperator! §

A metaoperator is basically an operator which takes another operator as argument, and augments it’s behaviour.

The simplest I can think of is the reduce metaoperator. Suppose you want to get the product of all items in a list. You know the operation you want, which is *, and in Ruby, Python, Smalltalk etc.. you would call a method or function called reduce or inject passing a function to it.

In Raku, you apply the prefix reduce metaoperator ([]) to the binary product operator (*):

> [*] [1,2,3]
6

The Zip metaoperator is the same:, it takes a binary operator and returns a binary operator, which applies its argument to items from both sides zipping them up:

> [1, 2, 3] Z* [10, 20, 30]
(10 40 90)

See where we’re going? Yep, we can apply the first metaoperator to the result of the second!§

> [Z*] [1, 2, 3], [10, 20, 30]
(10 40 90)

So, if we want to know “is the item in the left list larger than the corresponding in the right list?” we can just choose the right operator

> [Z>] [1, 2, 3, 1000], [10, 20, 30, 0]
(False False False True)

This means we can apply it to the slices of the original input to obtain a list of Booleans. Then we just have to count them, and you can do this easily by knowing that in Raku you can add Booleans, and they will be treated as 1 and 0.

Do you know how to add up all items in a list? Yep, reduce metaoperator and binary plus (+)!

So the full solution is

[+] [Z<] @ints, @ints[1..*];

Or in even shorter form

[+] [Z<] @ints[*,1..*]

This is at a glance impossible to understand, but it’s actually pretty expressive, and I guess it should get easier with habit, we’ll see 🙂

See you another day, happy hacking!

PS

Problem 2 left as an exercise for the reader. You may want to invest time in learning how to use hyper operators, they are cool!