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 itZ3.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
andvar <= 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 ofvar1 != 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[i1] + fib[i2]
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[i1] + fib[i2]
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 19
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:
$ ./sudoku
863579241
925314876
471826953
714683529
689752314
352491687
136245798
248937165
597168432
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 fixedsize 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)
declaredv
as 64bit 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
orZ3.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
I looked for some examples and found this one. Let's use Z3 to solve it!
#!/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 computerstyle fixedsized 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.).
Code
All code examples for the series will be in this repository.
Top comments (0)