Visualizing Z3's proofs

A writeup of a presentation I gave in class.

SMT solvers like Z3 are often also called automated theorem provers. Why? What do their proofs look like?

An SMT solver tells us if a formula in first-order logic (augmented with various theories) is satisfiable¹: there is some assignment of variables that makes the formula true. Z3 can even produce such an assignment.

from z3 import *

i = Int('i')
solve(i > 0)

[i = 1]

Not every formula is satisfiable, though. In that case, there are two possibilities.

Z3 can say unknown. This is the less interesting one. It means that Z3 ran out of time or memory, or the algorithm it uses to find the assignment is incomplete, or the problem itself is unsolvable in general. In other words, we don't know for sure if an assignment does not exist.

The other outcome is unsat. This is a much stronger statement than satisfiability, as it means that every assignment of variables must not work.

This has something of the flavour of proving a theorem, where we aim to convince ourselves that a formula is true for every assignment of variables.

We can connect these two views by expressing the theorem we want to prove instead as the non-existence of a refutation, or counterexample, to it. We do this by negating the formula and asking, "is it possible that there is some way for this formula not to be true?" unsat means no, i.e. the theorem is always true.

Z3's proofs

Z3 has facilities for explaining its deductions, in the form of proofs. Let's try them on a really simple theorem, $\exists a. a = a$.

from z3 import *

set_param(proof=True)
s = Solver()

a = Bool('a')
f = a == a
s.add(Not(f))

res = s.check()
print(res)
if res == sat:
  print(s.model())
else:
  p = s.proof()
  print(p)

Something to note that is that variables in SMT are implicitly existentially quantified. Therefore we are searching for a counterexample by seeing if $\forall a. a \neq a$ is satisfiable.

unsat
mp(asserted(Not(a == a)),
   trans(monotonicity(rewrite((a == a) == True),
                      Not(a == a) == Not(True)),
         rewrite(Not(True) == False),
         Not(a == a) == False),
   False)

Unsurprisingly, it is not. Z3 outputs a proof tree, which we can traverse and pretty-print.

Firstly, we see that the conclusion at the bottom is False. This may seem odd, but recall that the goal is to show that negation of the original theorem cannot be proved, so this is the only conclusion which makes sense.

Next, we see some of Z3's inference rules² in action. Our original goal is asserted. We have two instances of rewrite, where built-in equalities are used to simplify terms. There is an application of monotonicity, where we negate both sides. Finally we use the transitivity of equality and modus ponens to derive the conclusion.

Let's try $\exists a. a = \neg (\neg a)$.

And here's another for the linear arithmetic formula $\exists x y. 2 x \leq 3 y, y > x, x > 0$.

Clearly, these generated proofs quickly get too large to be comprehensible. They're also largely mechanical and not very meaningful. Still, it's intriguing to see the automated reasoning that Z3 performs.

A final point about the last one is the application of the rule th-lemma to derive the conclusion.

This is a theory lemma, a placeholder rule for a possibly-opaque decision from a theory solver.

If you want to generate these proofs yourself, the code is here.