Tutorial
Here we present several mini-examples of SMT problems.
Proving the validity of De Morgan's law
This example is borrowed from Microsoft's introduction to Z3 for propositional logic.
We say a formula is valid if it is true for every assignment of values to its variables. For example, z ∨ ¬z
is valid. (This is useful because a valid formula can provide a useful transformation or simplification of a logical expression.)
One famous transformation is De Morgan's law: a ∧ b = ¬(¬a ∨ ¬b)
. To show validity of De Morgan's law, we can construct the bidirectional implication a ∧ b ⟺ ¬(¬a ∨ ¬b)
. It suffices to show that the negation of this formula is unsatisfiable.
using Satisfiability
@satvariable(a, Bool)
@satvariable(b, Bool)
conjecture = iff(a ∧ b, ¬(¬a ∨ ¬b))
status = sat!(¬conjecture, solver=Z3()) # status should be :UNSAT
Implications
Suppose you have Boolean variables p
, q
and r
. We want to find out: if p
implies q
and q
implies r
((p ⟹ q) ∧ (q ⟹ r)
) will p
imply r
(p ⟹ r
)? We can use a SAT solver to check.
using Satisfiability
@satvariable(p, Bool)
@satvariable(q, Bool)
@satvariable(r, Bool)
conjecture = ((p ⟹ q) ∧ (q ⟹ r)) ⟹ (p ⟹ r)
status = sat!(¬conjecture, solver=Z3())
Since the status is UNSAT, there is no example that disproves the conjecture. We see that the variables have taken on the value nothing
.
println("p = $(value(p))")
println("q = $(value(q))")
println("r = $(value(r))")
Optimizing over integers
The knapsack problem is a famous NP-complete problem in which you are packing a bag that cannot exceed some maximum weight. Given a set of items with known value and weight, you want to pack a subset that maximizes the value.
A simpler version, illustrated in this classic XKCD strip, is to pack the bag to exactly its maximum weight (or spend a specific amount of money). In fact, the problem in the XKCD strip can be expressed as a linear equation over integers.
using Satisfiability
@satvariable(a[1:6], Int)
c = [215; 275; 335; 355; 420; 580]
expr = and(and(a .>= 0), sum(a .* c) == 1505)
sat!(expr, solver=Z3())
println("Result: $(value(a))")
println("Check: $(sum(value(a) .* c))")
Proving properties of fixed-size integer arithmetic
This example is from Microsoft's Z3 tutorial. A bitvector x
is a power of two (or zero) if and only if x & (x - 1)
is zero, where & is bitwise and. We prove this property for an 8-bit vector.
using Satisfiability
@satvariable(b, BitVector, 8)
is_power_of_two = b & (b - 0x01) == 0
# iff is_power_of_two holds, b must be one of 1, 2, 4, ... 128
expr = iff(is_power_of_two,
or(b == 2^i for i=0:7))
status = sat!(expr, solver=Z3())
println(status) # if status is SAT we proved it.