The Eager Approach for solving \( \Th \)-satisfiability is not very natural and/or compact for many theories.
For instance, how would you translate nonlinear arithmetic atoms into Boolean logic?
In the lazy approach we combine Boolean level reasoning with
theory-specific algorithms:
a CDCL SAT solver takes care of the propositional structure, treating the theory atoms as Boolean variables, and
a dedicated theory solver helps the SAT solver by handling the theory part.
The main features of the approach are that
the theory solvers see only conjunctions of \( \Th \)-literals and
thus do not have to handle disjunctions causing “case splits”, and
for unsatisfiable conjunctions,
the theory solver returns a \( \Th \)-conflict
and
the propositional abstraction of the \( \Th \)-conflict is learned by
the SAT solver.
Therefore, the SAT solver learns lemmas of the theory.
Due to the structure of the approach,
it is usually called the CDCL(\( \Th \)), DPLL(\( \Th \)), or “lemmas on demand” approach.
Below is a simplified schematic picture of the approach.
With more details:
The formula is in conjunctive normal form (CNF)
The CDCL SAT solver treats each \( \Th \)-atom \( A \)
as a propositional variable \( \Abs{A} \)
The \( \Th \)-literals in the partial models generated in the CDCL solver
are communicated to the theory solver for \( \Th \)
The theory solver
decides whether the current conjunction of \( \Th \)-literals is \( \Th \)-satisfiable
if no, returns a \( \Th \)-conflict, i.e., a subset of the communicated \( \Th \)-literals that is \( \Th \)-unsatisfiable
if yes, possibly return \( \Th \)-implied literals or, if requested, a \( \Th \)-model
The (abstractions of the) negations of the theory conflicts
returned by the theory solver
are used as learned clauses in the CDCL part.
Formally, we define theory conflicts as follows:
Definition: \( \Th \)-conflict
Let \( C \) be the set of \( \Th \)-literals currently
asserted in the theory solver.
A subset \( C’ \subseteq C \) is called a \( \Th \)-conflict
if \( \bigwedge_{l \in C’}l \) is \( \Th \)-unsatisfiable.
A (simple) interface for theory solvers could be as follows:
\( \TSinit{A_1,…,A_k} \) initializes the theory solver
to know which atoms \( A_1,…,A_k \) appear in the formula, and
to have the empty current conjunction \( C \).
\( \TSassert{l} \), where \( l = A_i \) or \( l = \neg A_i \),
asserts the \( \Th \)-literal \( l \),
i.e., updates the current conjunction \( C \) to \( C \land l \).
\( \TSretract{} \) removes the latest asserted literal,
i.e., updates the current conjunction \( C \land l \) to \( C \).
\( \TSisSat{} \) returns
\( \True \) if the current conjunction \( C \) is \( \Th \)-satisfiable, and
a \( \Th \)-conflict \( C’ \subseteq C \) such that \( C’ \) is \( \Th \)-unsatisfiable otherwise.
\( \TSgetModel{} \) returns a \( \Th \)-model for \( C \) (assuming that \( C \) is \( \Th \)-satisfiable).
Example
The animation below shows one possible execution of CDCL(\( \Th \))
for the \( \TEUF \)-formula
\begin{eqnarray*}
(\neg(x \Eq y) \lor \neg(y \Eq z)) &\land&\\\\
(\neg(y \Eq f(z)) \lor {g(x) \Eq g(f(z))}) &\land&\\\\
(\neg(y \Eq f(z)) \lor {z \Eq f(z)})
\end{eqnarray*}
Sometimes it is possible for the theory solver to deduce
the values for some non-asserted atoms based on those already asserted.
Definition
A \( \Th \)-literal \( l \) for which \( C \ThModels l \) holds,
\( C \) being the conjunction of currently asserted \( \Th \)-literals,
is called a \( \Th \)-implied literal.
Example
Consider the CNF formula
$$… \land (a \lor {x \Eq y}) \land (\neg(y \Eq f(z)) \lor c \lor g(y) \Eq g(z)) \land (\neg a \lor \neg(x \Eq z)) \land …$$
and assume that the literals
\( x \Eq y \),
\( y \Eq f(z) \), and
\( \neg(g(y) \Eq g(z)) \)
have been asserted.
In this case, the literal \( \neg(x \Eq z) \) is an \( \TEUF \)-implied literal
because \( (x \Eq y) \land (y \Eq f(z)) \land \neg(g(y) \Eq g(z)) \EUFModels \neg(x \Eq z) \).
This is because if \( x \Eq z \) would be true,
then \( x \Eq y \) and \( x \Eq z \) would imply \( y \Eq z \) and
thus \( g(y) \Eq g(z) \) as well, contradicting the literal \( \neg(g(y) \Eq g(z)) \).
If a theory solver reports a \( \Th \)-implied literal,
the CDCL SAT solver can then assign the value to the
propositional abstraction of the literal.
For the conflict analysis,
the CDCL SAT solver needs a reason for the assigned literal:
Definition
A \( \Th \)-explanation for each \( \Th \)-implied literal \( l \)
is a subset \( C’ \subseteq C \) of the asserted literals such that
\( C’ \ThModels l \).
Example: Continues
In the example above,
\( \Set{x \Eq y, \neg(g(y) \Eq g(z))} \) is a \( \TEUF \)-explanation for \( \neg(x \Eq z) \)
and
the CDCL SAT-solver interpretes this as the clause \( \Abs{x \Eq y} \land \neg\Abs{g(y) \Eq g(z)} \Implies \neg\Abs{x \Eq z} \),
i.e., \( \neg\Abs{x \Eq y} \lor \Abs{g(y) \Eq g(z)} \lor \neg\Abs{x \Eq z} \).
To support theory-implied literals,
we can augment our (simple) theory solver interface with the following methods:
\( \TSgetImplied{} \) returns a set of \( \Th \)-implied literals \( l \)
implied by the current conjunction
(i.e., literals \( l = A_i \) or \( l = \neg A_i \) not appearing in \( C \)
for which \( C \ThModels l \) holds).
\( \TSexplain{l} \) for a \( \Th \)-implied literal returns
a \( \Th \)-explanation for \( l \),
i.e., a subset \( C’ \subseteq C \) of the current conjunction
for which \( C’ \ThModels l \) holds.
