100 Languages Speedrun: Episode 23: Ruby Z3

Let's talk about something I made.

Once upon a time, "logic programming" was a big thing. The idea was to just give the computer a bunch of mathematical statements, and have it do the math and logic to arrive at answer. There were even whole languages like Prolog centered around this.

This approach basically died out. As it turns out logic programming languages are bad at everything other than logic. And it also turns out the forms of logic they're based on ("Horn clauses") are bad for logic as well.

The modern approach is to use general purpose programming language, and some kind of constraint solver engine (also known as theorem prover etc. - this field is really suffering from inconsistent terminology). In this episode we'll explore Microsoft Research's Z3. I didn't like any of its existing bindings, so I created Ruby bindings for it that I consider far superior, and we'll be covering this here.

Installation

To get Ruby Z3 going, you'll need to run these on OSX, or some obvious equivalent on other platforms. It's best to use latest version:

$ brew install z3
$ gem install z3

Getting Started

Let's write some very simple Z3 programs. Since you're probably new to constraint solvers, I'll go slow, as there will be a few concepts to explain on the way.

Let's try to solve 2 + X = 4.

#!/usr/bin/env ruby

require "z3"

solver = Z3::Solver.new
solver.assert 2 + Z3.Int("X") == 4

if solver.satisfiable?
  model = solver.model
  puts "X = #{model[Z3.Int("X")]}"
else
  puts "There are no solutions"
end

Which prints rather unsurprising:

$ ./x_plus_2_equals_4
X = 2

What is going on here?

first we create a solver instance - we'll generally create a new one for each problem we're solving
then we give the solver some equations
these equations contain variables, which are basically "symbols with types". Instead of saying 2 + Z3.Var("X") == 4 and telling it Z3.Var("X") is an integer separately, each variable carries both its name and its type (called "sort" in Z3, mostly to avoid confusion with programming language types).
once we're done, we ask Z3 if what it got is satisfiable?
if yes, we ask for a model - model is like a dictionary of assignments of variables to values. If there are many possible models, Z3 will only give us one.
then we ask the model what's the value of X and print it

Ruby allows operator overloading including == operator. This is much more readable than typing out something like Z3.Equals(Z3.Add(Z3.Number(2), Z3.Int("X")), Z3.Number(4))).

There are a few caveats. The biggest one is that and/&&, or/||, and ?: are not overloadable in Ruby, so we'd need to use & and | instead.

If you're curious, they cannot be regular methods - methods evaluate their arguments first, then run method code. In case of these, the right side evaluates or doesn't depending on what the left side does.

SEND + MORE = MONEY

Let's try another quick one, the famous "verbal arithmetic puzzle" SEND+MORE=MONEY. Every letter stands for a different digit, and initial digits cannot be zero.

#!/usr/bin/env ruby

require "z3"

solver = Z3::Solver.new
letters = %w[s e n d m o r e m o n e y].uniq.to_h{|letter| [letter, Z3.Int(letter)]}

letters.each_value do |var|
  solver.assert var >= 0
  solver.assert var <= 9
end

solver.assert letters["m"] != 0
solver.assert letters["s"] != 0

solver.assert Z3.Distinct(*letters.values)

send = 1000 * letters["s"] + 100 * letters["e"] + 10 * letters["n"] + letters["d"]
more = 1000 * letters["m"] + 100 * letters["o"] + 10 * letters["r"] + letters["e"]
money = 10000 * letters["m"] + 1000 * letters["o"] + 100 * letters["n"] + 10 * letters["e"] + letters["y"]

solver.assert send + more == money

if solver.satisfiable?
  model = solver.model
  model.each do |var, value|
    puts "#{var}=#{value}"
  end
  puts "#{model[send]} + #{model[more]} = #{model[money]}"
else
  puts "There are no solutions"
end

Which prints:

$ ./send_more_money
d=7
e=5
m=1
n=6
o=0
r=8
s=9
y=2
9567 + 1085 = 10652

There's a lot going on here, so let's take it step by step:

writing Z3.Int(letter) can get rather tedious, so I created a dictionary {"s" => Z3.Int("s"), ...} to make the code a bit more concise.
for every letter variable, we tell the solver that var >= 0 and var <= 9
for initial letter variables, we tell the solver that they're not 0, as per rules of the puzzle
not everything can use operator overloading - for example to tell the solver that all variables are distinct, we use special Z3.Distinct(var1, var2, ...) instead of double nested loop of var1 != var2
we calculate what would SEND, MORE, and MONEY be with just some normal * and +
we check if it's satisfiable
if yes, we ask for a model
we can do interesting thing with the model - we can ask it to print all variables it knows about and their values
but the model can also evaluate expressions (if they only use known variables) like SEND, MORE, and MONEY

The whole code is just delightful.

Fibonacci

Z3 has support for many very fancy things like functions, sets, and so on, but it's best if we limit ourselves to just simplest sorts for now. For an extremely simple Fibonacci solver, let's just declare integer variables called "fib(0)" to "fib(100)":

#!/usr/bin/env ruby

require "z3"

solver = Z3::Solver.new

fib = (0..100).map{|i| Z3.Int("fib(#{i})")}

solver.assert fib[0] == 0
solver.assert fib[1] == 1

(2..100).each do |i|
  solver.assert fib[i] == fib[i-1] + fib[i-2]
end

if solver.satisfiable?
  model = solver.model
  fib.each do |var|
    puts "#{var}=#{model[var]}"
  end
else
  puts "There are no solutions"
end

Which prints just what we'd expect:

$ ./fib
fib(0)=0
fib(1)=1
fib(2)=1
fib(3)=2
fib(4)=3
fib(5)=5
fib(6)=8
fib(7)=13
fib(8)=21
fib(9)=34
fib(10)=55
fib(11)=89
fib(12)=144
fib(13)=233
fib(14)=377
fib(15)=610
fib(16)=987
fib(17)=1597
fib(18)=2584
fib(19)=4181
fib(20)=6765
...
fib(90)=2880067194370816120
fib(91)=4660046610375530309
fib(92)=7540113804746346429
fib(93)=12200160415121876738
fib(94)=19740274219868223167
fib(95)=31940434634990099905
fib(96)=51680708854858323072
fib(97)=83621143489848422977
fib(98)=135301852344706746049
fib(99)=218922995834555169026
fib(100)=354224848179261915075

We didn't have to tell Z3 how to evaluate this series, just how the variables are related to each other. Z3 Integers have unlimited size, and it's super fast (<0.1s on my laptop, mostly just startup time).

Reverse Fibonacci

That's probably not too impressive, so let's try something fancier. What if we only told Z3 what's fib(42) and fib(69) and asked it for the rest?

#!/usr/bin/env ruby

require "z3"

solver = Z3::Solver.new

fib = (0..100).map{|i| Z3.Int("fib(#{i})")}

solver.assert fib[42] == 267914296
solver.assert fib[69] == 117669030460994

(2..100).each do |i|
  solver.assert fib[i] == fib[i-1] + fib[i-2]
end

if solver.satisfiable?
  model = solver.model
  fib.each do |var|
    puts "#{var}=#{model[var]}"
  end
else
  puts "There are no solutions"
end

Yes, that works just as well as the previous version, printing identical output!

Sudoku Solver

The Sudoku Solver is the FizzBuzz equivalent for constraint solvers, so let's write one!

#!/usr/bin/env ruby

require "z3"

sudoku = %w[
  _6_5_9_4_
  92_____76
  __1___9__
  7__6_3__9
  _________
  3__4_1__7
  __6___7__
  24_____65
  _9_1_8_3_
]

solver = Z3::Solver.new

vars = (0..8).map{|y|
  (0..8).map{|x|
    Z3.Int("cell[#{x},#{y}]")
  }
}

# All cells are 1-9
vars.flatten.each do |var|
  solver.assert var >= 1
  solver.assert var <= 9
end

# Cells match sudoku grid if it already has numbers
9.times do |y|
  9.times do |x|
    if sudoku[y][x] =~ /\d/
      solver.assert vars[y][x] == sudoku[y][x].to_i
    end
  end
end

# Each row has distinct numbers
vars.each do |row|
  solver.assert Z3.Distinct(*row)
end

# Each column has distinct numbers
vars.transpose.each do |col|
  solver.assert Z3.Distinct(*col)
end

# Each box has distinct numbers
[0, 3, 6].each do |i|
  [0, 3, 6].each do |j|
    cells = vars[i, 3].flat_map{|row| row[j, 3]}
    solver.assert Z3.Distinct(*cells)
  end
end

if solver.satisfiable?
  model = solver.model
  9.times do |y|
    9.times do |x|
      print model[vars[y][x]]
    end
    print "\n"
  end
end

And it does exactly what we want:

The example is a bit longer, but there's nothing complicated here, it's just a list of assertions about what we want, Z3 does some Underpants Gnomes Magic, and then we print the result and profit!

Since we're using Ruby, it would be very easy to extend it with reading sudoku from a file, any kind of fancy formatting, or putting it as a web service. This is something logic programming languages like Prolog really struggled wit, but general purpose lanugages are great at.

Proving facts about Bit Vectors

After integers and booleans, the next most common sort would likely be fixed-size integer bit vectors, that is signed and unsigned ints used in most lower level programming languages.

Theorem provers can be used in a few ways. The way we used Z3 so far is by feeding it a list of assertions. It then either constructs a model that satisfies the assertions, or it proves that it's impossible (... or takes million years to finish so you'll never know).

Sometimes we're interested in the model, and theorem prover telling us it can't be done is sort of a fail, like Sudoku that's impossible to solve.

But sometimes we want the opposite. We want to make sure X is true. So we send Z3 a list of assertions, then we send it not X, and ask for a model. If it says imposible, then this proves X. Otherwise the model is the counterexample, so we not only know X is not always true, but we have an example for it.

Let's take one simple bit trick from the Bit Twiddling Hacks site, and implement it incorrectly - "Determining if an integer is a power of 2".

#!/usr/bin/env ruby

require "z3"

solver = Z3::Solver.new
v = Z3.Bitvec("v", 64)

naive_is_power_of_two = Z3.Or(*(0..63).map{|i| v == 2**i})
tricky_is_power_of_two = (v & (v - 1)) == 0

theorem = (tricky_is_power_of_two == naive_is_power_of_two)

solver.assert !theorem

if solver.satisfiable?
  counterexample = solver.model
  puts "Counterexample exists:"
  counterexample.each do |n,v|
    puts "* #{n} = #{v}"
  end
else
  puts "There are no counterexamples, it always holds."
end

And let's give it a go:

$ ./power_of_two
Counterexample exists:
* v = 0

Damn, the theorem is wrong, and doesn't hold for v = 0!

Let's walk through the code:

Z3.Bitvec("v", 64) declared v as 64-bit bit vector (int64 or such in most low level languages). Z3 doesn't distinguish between "signed" and "unsigned" bitvectors - for operations where it matters like >, it provides .signed_gt and .unsigned_gt versions, but most things (+, *, ==, &, |) etc. work the same.
we construct naive_is_power_of_two as (v == 1) | (v == 2) | (v == 4) | ... | (v == 2**63). Z3.Or(s1, s2, s3, ...) is a shortcut, as it's very common code. As I mentioned before, Ruby's || cannot be overloaded so we need to use either | or Z3.Or.
we construct tricky_is_power_of_two to be our trick operation. For bitvectors, Z3 provides bit operations like &, |, ^ etc., in addition to regular arithmetic. Z3 generally cannot do bit operations on unlimited size integers.
we ask Z3 if it can give us any example where our theorem tricky_is_power_of_two == naive_is_power_of_two could be false
and it does

Let's try to fix it:

#!/usr/bin/env ruby

require "z3"

solver = Z3::Solver.new
v = Z3.Bitvec("v", 64)

naive_is_power_of_two = Z3.Or(*(0..63).map{|i| v == 2**i})
tricky_is_power_of_two = (v != 0) & ((v & (v - 1)) == 0)

theorem = (tricky_is_power_of_two == naive_is_power_of_two)

solver.assert !theorem

if solver.satisfiable?
  counterexample = solver.model
  puts "Counterexample exists:"
  counterexample.each do |n,v|
    puts "* #{n} = #{v}"
  end
else
  puts "There are no counterexamples, it always holds."
end

And this time it works:

$ ./power_of_two_2
There are no counterexamples, it always holds.

It would be completely impractical to brute force check all 2**64 possible values, but for Z3 it's no big deal.

Physics Textbook Problems

#!/usr/bin/env ruby

# A race car accelerates uniformly from 18.5 m/s to 46.1 m/s in 2.47 seconds.
# Determine the acceleration of the car and the distance traveled.

require "z3"

solver = Z3::Solver.new

a = Z3.Real("a")
v0 = Z3.Real("v0")
v1 = Z3.Real("v1")
t = Z3.Real("t")
d = Z3.Real("d")

solver.assert a == (v1 - v0) / t
solver.assert v0 == 18.5
solver.assert v1 == 46.1
solver.assert t == 2.47
solver.assert d == (v0 + v1) / 2 * t

if solver.satisfiable?
  model = solver.model
  model.each do |var, value|
    puts "#{var}=#{value}"
  end
else
  puts "There are no solutions"
end

Let's give it a try:

$ ./physics
a=2760/247
d=79781/1000
t=247/100
v0=37/2
v1=461/10

For Real numbers, Z3 will use exact rational form by default. You can turn them into fixed floating point numbers for display with .to_f.

Z3 also has computer-style fixed-sized floats, if you want to prove some facts about Quake's inverse square root algorithm.

I could be going, but the episode is already quite long. Z3 gem comes with many examples, including crazy things like Regular Expression Crossword Solver - which takes a crossword where the hints are regular expressions and cells are letters, and figures out the solution.

Should you use Z3?

Absolutely! Z3 is the best constraint solver engine out there, and it's very popular for serious uses like hacking CTF competitions.

When using Z3 or any other constraint solver, it's important to remember than performance can be extremely unpredictable. Some sets of constraints can be solved in a few seconds, while others can take days, even though they look very similar. If you let users throw data at your constraint solver, it's best to put it in a separate process, with proper timeouts and error handling.

Should you use Ruby Z3?

Z3 comes with a few officially supported languages, of which the only one worth considering is Python. I didn't love that version, so I created Ruby bindings, which I think are a bit better overall, but nobody can fault you if you prefer Python.

There's a small issue that Z3 has some experimental features which aren't very stable from version to version, so the Ruby gem might take longer to update than officially maintained Python version. But that doesn't affect any of the common use cases (like booleans, integers, bit vectors, reals, floats etc.).