CpSc 538G: SMT Solvers: An appetizer; Intro, and applications
September 14, 2016
I. Introduction
A. Big picture
1. "Satisfiability Modulo Theories: An Appetizer" sketches
a. the mathematical logic of SMT
b. the implementation techniques for writing an SMT solver
c. applications are mentioned, but the detail is light.
2. "Satisfiability Modulo Theories: introduction and applications"
a. Presents several, simple, motivating examples
b. describes how SMT solvers can handle problems whose
representations span several domains.
c. gives less detail about how these actually work.
B. Today's lecture
1. I'll focus on the sketch of how an SMT solver works.
a. We've already seen a few examples:
exploit generation and puzzle solving
b. As noted in "Automatic Exploit Generation", we eventually need
to understand how this stuff works to apply these techniques
to large scale problems.
2. I'll look a bit at the examples at the end.
II. "An Appetizer" -- the anatomy of a SMT solver
A. Overview
0. What is the thesis of the paper:
SMT combines fundamental work in mathematical logic (esp. decision
procedures) with careful software implementation to produce powerful
tools for software engineering problems.
1. The paper first describes the mathematical logic of SMT (Section 2)
a. What is many-sorted, first-order logic
b. What "modulo theories" means
c. What is a model for a formula.
d. CNF, quantifiers, uninterpreted functions, etc.
2. The rest of the paper sketches how SMT solvers work in practice:
a. SAT: efficient case analysis (Sec. 3)
b. Other theories (Sec. 4)
c. SAT + a theory solver (Sec. 5)
d. Integrating multiple theory solvers (Sec. 6)
e. Some stuff about meta-procedures.
B. The mathematical logic of SMT
1. Propositional logic:
a. formula is:
a variable
Not(phi), where phi is a formula
And(phi1, phi2), where phi1 and phi2 are formulas
Or(phi1, phi2), where phi1 and phi2 are formulas
Implies(phi1, phi2), where phi1 and phi2 are formulas
Equal(phi1, phi2), where phi1 and phi2 are formulas
b. The *semantics* of a formula tells us the "meaning" of the formula.
For propositional formulas, this is the "obvious" meaning.
Let M be an assignment of values to variables.
If evaluating the formula with these values according to the
usual meaning of NOT, AND, OR, IMPLIES, and EQUIV produces
'true', then we write: M |= phi and say that M is a model
of phi.
If phi has a model (i.e. some assignment of values to variables
satisfies phi), then we say that phi is satisfiable.
For example,
And(And(Or(x, Not(y)), Or(y, Not(z))), Or(z, Not(x)))
is satisfiable, but
And(And(And(And(Or(x, Not(y)), Or(y, Not(z))),
Or(z, Not(x))), Or(x, y)), Or(Not(y), Not(z)))
is not.
I wrote all of those 'And's because I defined And to be a
function with two arguments. To make this stuff easier to
read, I'll write:
And(x1, x2, x3, x4, x5)
as a shorthand for
And(And(And(And(x1, x2), x3), x4), x5)
and likewise with Or.
c. Two formulas, phi1 and phi2, are "equisatisfiable" iff both
are satisfiable, or both are not.
This is useful because we might want to know if phi1 is
satisfiable. We might not have a good way to reason about phi1
directly, but we have a way to convert it into phi2, where phi1
and and phi2 are equisatisfiable. If we have a decision procedure
for phi2, then we can use that to decide whether or not phi1 is
satisfiable.
Typically, a satisfying assignment for phi2 can be used to
construct a satisfying assighment for phi1.
Example, we can convert any Boolean formula into conjunctive normal
form (CNF) in linear space by adding new variables. The solution to
the CNF formula can be used to get a solution to the original.
c. CNF -- conjunctive normal form
A literal is a variable, or a negation of a variable:
If x and y are variables, then
x is a literal
Not(y) is a literal
Or(x, Not(y)) is not a literal
A clause is a disjunction of literals:
If a, b, c, d, e, f, ... z, are variables then:
Or(x, y) is a clause
Or(a, b, Not(c), e, Not(p), Not(q), r, Not(x), z) is a clause
Not(p) is a clause.
And(a, b) is not a clause
A CNF formula is conjunction of clauses:
And(And(Or(x, Not(y)), Or(y, Not(z))), Or(z, Not(x)))
is a CNF formula
And(Or(p, x), Or(p, y), Or(q, x), Or(q, y)) is a CNF formula
Or(And(p, q), And(x, y)) is not a CNF formula
d. Why do we care about CNF?
It provides a convenient form for SAT solvers.
In particular, SAT solvers can record their intermediate
progress as new clauses.
2. Many-sorted first-order logic
Like propositional logic, but we add other "sorts" (think "types"
or "domains"), functions, predicates, and quantifiers.
a. Sorts
We may want to talk about "things" that aren't booleans: e.g.
animals, countries, flowers, puns, etc. In software, we would
introduce "types". In mathematics, we typically use sets,
e.g. the set of all integers, the set of real numbers, etc.
I'm not sure I've got this 100% right (I'll need to bounce
this off of a logician or two). My understanding is that in
the context of logic, what we know about some "sort" are the
axioms that we use to describe it.
b. functions -- they're uninterpreted
Each function has a signature given by the number and sorts
of its arguments and the type of its result.
A "variable" is technically a function of zero arguments and
is called "an uninterpretted constant".
c. predicates -- pretty much a function whose range is the booleans.
A propositional variable is a predicate of zero arguments.
d. signatures: a signature is a tuple (Sigma, F, P)
where Sigma is a set of sorts; F is a set of functions
each described by its arity; and P is a set of predicates,
again with each described by its arity.
e. terms, atoms, and formulas:
terms: function applications where the arguments are of
the required sorts. Can be a variable as described above.
atoms: predicates where the arguments are of the required
sorts. Can be a propositional variable as described above.
formulas: a formula is an atom, a boolean combination of formulas,
or a quantified (exists or for-all) formula.
f. signatures and structures -- getting to what formulas mean.
The idea of satisfiability extends to formulas in the many-sorted
logic. A structure consists of:
1. A domain (i.e. a set) for each sort -- often "obvious"
2. A mapping for each function for the values in the given domains.
If phi is a formula and M is a structure, we write M |= phi if phi
is satisfied by M. For this introduction, we'll just say that
all of the operations are handled in the "obvious way".
g. Satisfiability and validity:
Satisfiability:
Given a signature, Sig, and a formula phi, we say that phi
is satisfiable if M |= phi for some structure M of Sig.
Validity:
Given a signature, Sig, and a formula phi, we say that phi
is valid if M |= phi for every structure M of Sig.
h. Skolemization:
A way to handle existential quantifiers using uninterpreted
functions.
i. Conversion to CNF and universal quantifiers.
I had to read this part many times before it made sense.
Here's what I believe they are trying to say:
Given an arbitrary, many-sorted, first-order logic formula,
we want to convert it to CNF so we can use our SAT/SMT
algorithms. Most of this can be done using the
transformations described earlier. However, universal
quantifiers require a bit of extra attention.
Let's say that a formula has a sub-formula of the form
ForAll x: sort. phi
where phi not in CNF. If we didn't have the 'ForAll',
we could use the methods described earlier to convert phi
to CNF. The observation is that with the quantifier,
we can convert phi into a conjunction of clauses, where
some of the clauses are of the form:
ForAll x: sort. Or(a_1, ..., a_n)
where a_1, ..., a_n are atoms.
j. Phew! Glad that's done.
III. Solving SAT problems
A. DPLL: explore the decision tree
1. If making a choice for a variable leaves a clause
a. satisfied: great, simplify the formula by dropping the clause
that is the only possible candidate. This can enable further
simplifications.
b. with one atom -- it's a unit clause.
DPLL chooses an assignment for that atom
c. with zero atoms -- it's a conflict clause.
the clause is unsatisfiable.
DPLL can backtrack and doesn't need to explore the
rest of the subtree.
2. Continue exploring the tree until
a. A satisfying assignment is found, or
b. A conflict is found with no decisions to backtrack
In this case, the formula is unsatisfiable.
B. Modern SAT solvers improve on DPLL with
a. Clause learning
b. non-chronological backtracking
c. Indexing schemes for fast unit propoagation and
fast conflict detection.
III. Adding other theories to SAT
A. Other theories are expressed as predicates.
1. The SAT solver proposes truth values for these predicates
2. The theory solver reports whether or not this truth assignment
is consistent with the theory.
3. If the SAT solver finds an assignment that is consistent with
all of the other theories, we've got a satisfying assignment
for the entire formula. Note that the theory solvers give
us the witness values for the variables for their domains.
4. If one or more theory solvers refute the proposed assignment,
they return conflict clauses to the SAT solver, and the SAT
solver tries again.
5. If the SAT solver can't find an assignment, then the problem
is unsatisfiable.
B. An example:
1. Let
a. p, q be boolean variables
b. x, y, z be real valued variables
2. Is
And(x >= 0, z >= 1,
If(p, x*x + z*x + y == 0, x+z < y),
Implies(q, y < 1),
Or(p, q))
satisfiable?
a. Create a new boolean variable for each inequality:
v1 = (x >=0),
v2 = (z >= 1),
v3 = (x*x + z*x + y == 0)
v4 = (x+z < y),
v5 = (y < 1),
b. The boolean version of the problem is
And(v1, v2,
If(p, v3, v4),
Implies(q, v5),
Or(p, q))
c. The SAT solver gives a solution:
And(p, Not(q), v1, v2, v3, v4, Not(v5))
d. The corresponding real-arithmetic problem is:
And(x >= 0, z >= 1, x*x + z*x + y == 0, Not(x+z < y), Not(y < 1))
which is unsatisfiable. We try dropping clauses one at a time from
left to right to get a minimal, unsatisfiable problem:
J = Not(And(x >= 0, x*x + z*x + y == 0, Not(x+z < y), Not(y < 1)))
= Or(Not(x >= 0), Not(x*x + z*x + y == 0), x+z < y, y < 1))
= Or(Not(v1), Not(v3), v4, v5)
e. Add the clause for J to our boolean problem and solve again:
And(v1, v2,
If(p, v3, v4),
Implies(q, v5),
Or(p, q),
Or(Not(v1), Not(v3), v4, v5))
to get the solution
And(Not(p) q, v1, v2, Not(v3), v4, v5)
f. Try the corresponding real-arithmetic problem
And(x >= 0, z >= 1, Not(x*x + z*x + y == 0), x+z < y, y < 1)
which is unsatisfiable, with the justification
J = Not(And(x >= 0, z >= 1, x+z < y, y < 1))
= Or(Not(v1), Not(v2), Not(v4), Not(v5))
g. Add the new clause to the boolean problem and solve again:
And(v1, v2,
If(p, v3, v4),
Implies(q, v5),
Or(p, q),
Or(Not(v1), Not(v3), v4, v5),
Or(Not(v1), Not(v2), Not(v4), Not(v5)))
to get the solution
And(p, Not(q), v1, v2, v3, Not(v4), v5)
h. Try the corresponding real-arithmetic problem
And(x >= 0, z >= 1, x*x + z*x + y == 0, Not(x+z < y), y < 1)
and we get a solution with [x=1, z=2, y=-3].
i. Combine the boolean and real-arithmetic solutions to get
[p=True, q=False, x=1, z=2, y=-3]
as a solution to the original problem:
And(x >= 0, z >= 1,
If(p, x*x + z*x + y == 0, x+z < y),
Implies(q, y < 1),
Or(p, q))
C. Improvements
1. Theory solvers that can work with partial assignments:
a. Report that the partial assignment is unsatisfiable
b. Report clauses that are simplied by the partial assignment.
c. Example: a linear-difference arithmetic solver (very fast) can show
Not(And(x >= 0, x >= 1, x+z < y, y < 1)).
This tells the SAT solver
Or(Not(v1), Not(v2), Not(v4), Not(v5))
Let's write the original, boolean problem in CNF, and add this clause
And(v1, v2,
Or(Not(p), v3), Or(p, v4), % If(p, v3, v4)
Or(Not(q), v5), % Implies(q, v5)
Or(p, q),
Or(Not(v1), Not(v2), Not(v4), Not(v5)))
And(v1, v2) must hold in any solution, and the SAT solver can
learn the clause, Or(Not(v4), Not (v5)). We now have
And(v1, v2,
Or(Not(p), v3), Or(p, v4), % If(p, v3, v4)
Or(Not(q), v5), % Implies(q, v5)
Or(p, q),
Or(Not(v4), Not(v5)))
If we try Not(p) holds, then unit propagation shows that
v4 and v5 both hold, and Or(Not(v4), Not(v5)) is a conflict
clause. We backtrack and learn the clause p. Eliminating
the satisfied clauses yields:
And(p, v1, v2,
Or(Not(p), v3),
Or(Not(q), v5),
Or(Not(v4), Not(v5)))
Now perform unit propagation:
And(p, v1, v2, v3,
Or(Not(q), v5),
Or(Not(v4), Not(v5)))
From here, we can either find a solution to the SAT problem,
and try it in the real-arithmetic solver, or we can ask a
real-arithmetic solver what it can infer about v4 and v5 given
And(v1, v2, v3). Note that Implies(And(v1, v2, v3), y < 0)),
from which we can conlude And(Not(v4), v5), and the rest is simple.
2. Incremental theory solvers:
Speed matters.
In the example above, we could have already asked the arithmetic
solver about And(v1, v2). When the SAT solver learned v3, we can
add this fact to an incremental, arithmetic solver to conclude
Not(v4), v5.
IV. Combining theories
A. How do the theories interact?
1. Only with equality terms: well-understood.
2. Other shared symbols: much more complicated.
B. The basic idea of Nelson-Oppen
1. Theory solvers find equalities, these can be propagated to
the other theory solvers.
2. For unresolved equality constraints, the theory combiner
needs to check "all" combinations.
3. An example would be good.
4. A few remarks about delayed theory combination, etc.
C. A few more technical terms
1. Stably infinite:
a. Formally: "A theory, T, is stably infinite with respect
to sort sigma if for every formula phi that is satisfiable
in T, there exists a structure, M, s.t. M |=_T phi and
|M|_sigma is infinite."
b. Informally, T is stably infinite wrt. sigma if for
any satisfiable formula, phi, we can find a model
where the domain for sigma is infinite. This makes
handling equality constraints easier because we don't
need to worry about running out of distinct values.
2. Convex theories:
Let S be a set of literals, and E be some non-empty
set of equalities over variables. Theory T is convex if
(S implies Exists e: E. e) in T
implies there exists e In E such that
(S implies e) in T
V. Some examples