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'

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 =

# 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
  puts "I can't solve that, Dave"

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 =

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>
  puts "I can't do that Dave"

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 =

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

# 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" do |char|
    var = variables[char]
    print values[var] || char
  p "Impossibru!"

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

# create a hash monkey-name -> variable 
# so we can look them up by name
env = { |h, k| h[k] = Z3.Int(k) }

# convert the input to a ruby program 
prog = 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")

solver =
# ger the program in here

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

Ruby, RVM, MacPorts and OpenSSL on macOS (Monterey)

This is not so much a blog post but a log for the sake of future Me:

I have been using MacPorts on macOS for many years and am 99% happy with it: it allows installing binary packages and source ones with custom options, allows multiple versions to live side by side, has a lot of packages, can dump the whole list of installed stuff so you can re-install it elsewhere easily and many other things. It’s great.

I have also for a long time used RVM as my ruby version manager of choice. Again, it just works.

An issue with installing older rubies in recent macOS is that the system-provided OpenSSL is version 3, and ruby before 3.1 cannot build against it.

You can get OpenSSL1.0 or 1.1 via MacPorts, but there’s another problem: when you try to install anything recent via MacPorts you will end up with OpenSSL3, and at that point you will have problems building old ruby versions or old versions of gems like eventmachine or puma, expecting to have OpenSSL1.

This problem manifests itself when installing ruby 2.7 via RVM with a build/install log that ends like this

/Users/riffraff/.rvm/src/ruby-2.7.6/lib/rubygems/core_ext/kernel_require.rb:83:in `require': cannot load such file -- openssl (LoadError)
        from /Users/riffraff/.rvm/src/ruby-2.7.6/lib/rubygems/core_ext/kernel_require.rb:83:in `require'
        from /Users/riffraff/.rvm/src/ruby-2.7.6/lib/rubygems/specification.rb:2430:in `to_ruby'
        from ./tool/rbinstall.rb:846:in `block (2 levels) in install_default_gem'
        from ./tool/rbinstall.rb:279:in `open_for_install'
        from ./tool/rbinstall.rb:845:in `block in install_default_gem'
        from ./tool/rbinstall.rb:835:in `each'
        from ./tool/rbinstall.rb:835:in `install_default_gem'
        from ./tool/rbinstall.rb:799:in `block in <main>'
        from ./tool/rbinstall.rb:950:in `block in <main>'
        from ./tool/rbinstall.rb:947:in `each'
        from ./tool/rbinstall.rb:947:in `<main>'

the ruby binary is actually built correctly but the openssl extension failed to build, which you can tell by looking back in the build history

*** Following extensions are not compiled:
         Could not be configured. It will not be installed.
         Check ext/openssl/mkmf.log for more details.

If you look into .rvm/src/ruby-2.7.6/ext/openssl/mkmf.log you will find

/Users/riffraff/.rvm/src/ruby-2.7.6/ext/openssl/extconf.rb:111: OpenSSL >= 1.0.1, < 3.0.0 or LibreSSL >= 2.5.0 is required

So it seems to have ruby use OpenSSL1 you should uninstall OpenSSL3 and everything that depends on it.

FWIW, I think that works, but it’s not ideal.

But fear not! There’s a better solution! You just need to tell RVM (and ruby) to use look for headers and libraries in the right place.

To do this you need to both specify where pkgconfig is and which openssl directories to use.

Luckily, this is not difficult, follow this incantation

$ PKG_CONFIG_PATH=/opt/local/lib/openssl-1.1/pkgconfig rvm reinstall 2.7.6 --with-openssl-lib=/opt/local/lib/openssl-1.1 --with-openssl-include=/opt/local/include/openssl-1.1

You effectively have to tell ruby how to configure itself, and how to find OpenSSL1 at compile time and at link time.

In theory --with-openssl-dir should be enough, but AFAIU MacPorts puts stuff in separate directories which does not play well with ruby-build. Which is fair, as ruby-build does not explicitly support MacPorts, but rather homebrew.

Anyway, once this is solved you may still encounter issues when installing gems that depend on OpenSSL, as those will also need to be told where OpenSSL is.

For example,. this is the error I get installing puma 5.6.4

compiling puma_http11.c
linking shared-object puma/puma_http11.bundle
Undefined symbols for architecture arm64:
  "_SSL_get1_peer_certificate", referenced from:
      _engine_peercert in mini_ssl.o
ld: symbol(s) not found for architecture arm64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [puma_http11.bundle] Error 1

make failed, exit code 2

The equivalent error for eventmachine would be something like

linking shared-object rubyeventmachine.bundle
Undefined symbols for architecture arm64:
  "_SSL_get1_peer_certificate", referenced from:
      SslBox_t::GetPeerCert() in ssl.o
ld: symbol(s) not found for architecture arm64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [rubyeventmachine.bundle] Error 1

Luckily you the same technique works to install older gems that need OpenSSL1. Notice you need an extra -- to separate the arguments provided to the gem configuration script from the ones to the gem command.

$ PKG_CONFIG_PATH=/opt/local/lib/openssl-1.1/pkgconfig gem install puma -v '5.6.4' -- --with-openssl-lib=/opt/local/lib/openssl-1.1 --with-openssl-include=/opt/local/include/openssl-1.1

(also worth noting: puma 5.6.5 builds without problems, see this and this)

So, hopefully I will be able to forget old code that relies on OpenSSL1 at some point, but in case I need it again: hey future Me, this is how you workaround the issue!

A note on ruby 3.0

If you build ruby 3.0 with MacPorts it will not explode, but it will not build the OpenSSL extesion, in /Users/riffraff/.rvm/src/ruby-3.0.4/ext/openssl/mkmf.log you will find the same error you’ve just seen

/Users/riffraff/.rvm/src/ruby-3.0.4/ext/openssl/extconf.rb:113: OpenSSL >= 1.0.1, < 3.0.0 or LibreSSL >= 2.5.0 is required
	/Users/riffraff/.rvm/src/ruby-3.0.4/ext/openssl/extconf.rb:113:in `<top (required)>'
	./ext/extmk.rb:214:in `load'
	./ext/extmk.rb:214:in `block in extmake'
	/Users/riffraff/.rvm/src/ruby-3.0.4/lib/mkmf.rb:331:in `open'
	./ext/extmk.rb:210:in `extmake'
	./ext/extmk.rb:572:in `block in <main>'
	./ext/extmk.rb:568:in `each'
	./ext/extmk.rb:568:in `<main>'

and this in turn will mean you can’t build puma or eventmachine or other things that depend on the ruby openssl extension

$ gem install puma
ERROR:  While executing gem ... (Gem::Exception)
    OpenSSL is not available. Install OpenSSL and rebuild Ruby (preferred) or use non-HTTPS sources

But you’re good, the same solution as before will allow you to install that version of ruby too

$ PKG_CONFIG_PATH=/opt/local/lib/openssl-1.1/pkgconfig rvm install 3.0 --with-openssl-lib=/opt/local/lib/openssl-1.1 --with-openssl-include=/opt/local/include/openssl-1.1

From ruby 3.1 onwards, ruby will build just fine with the system-provided OpenSSL3, so you will be able to avoid these shenanigans.

You can still build against MacPorts’ version of OpenSSL1 or OpenSSL3 by using the right paths.

Happy hacking future Me!

Building ruby 2.7 on macOS with MacPorts and OpenSSL3

Recently I got a new apple box (an M1 MacBook Pro, which is nice, if a bit bulky), and found myself in the need to re-establish my dev environment.

This meant re-compiling various old ruby versions which I need for some projects. The problem is old ruby releases before ruby 3 required an equally ancient version of OpenSSL

I have used RVM for many years and it has a nice integration with MacPorts, my favorite macOS package manager. Getting the ports I need on a new install is straightforward, you just get a list of installed packages from one machine and reinstall them on the other. And RVM knows how to get rubies when you encounter a .ruby-version file, so no issue there.

But there’s a catch: I am using OpenSSL3 for most of my stuff, but I need OpenSSL1.0 or 1.1 to build ruby 2.7.5 and older.

If you google this, you will find plenty of bug reports against RVM, ruby-install, puma and plenty of others, with varying suggestion to use --with-openssl-dir, or setting PKG_CONFIG_PATH, overriding LD_FLAGS, and other incantations.

These may work in some cases, but not all: it seems an underlying problem is that if you have multiple versions of OpenSSL the ruby configure script may end up overriding the openssl-dir setting, and still end up linking against the incorrect library.

Luckily, the solution is pretty straightforward if you ignore all those recommendations 🙂

Try this

  • Install OpenSSL3: sudo port install openssl3
  • Install Ruby 3: rvm install 3.1
  • Check that it works and it loads openssl fine, by running something like ruby -ropenssl -e 'p [RUBY_VERSION, OpenSSL::VERSION]'
  • Install OpenSSL1 sudo port install openssl1
  • Remove v3: sudo port uninstall openssl3 (keep things that depended on it if you want)
  • Install older rubies: rvm install 2.7.5
  • Check those work too
  • Reinstall openssl3

Everything should now work fine, because MacPorts has no issues with multiple library versions sitting next to each other, and each ruby is linked to the appropriate one. Packages that depend on V1 or V3 will also just be happy next to each other.

Notice, I did this once already almost a year ago, and I had totally forgotten about it.

So here’s this small post, in the hope it may help someone, or at least my future self.