Craig interpolation

If A implies B, there is a formula I using only the symbols A and B share, with A implying I and I implying B. In verification the equivalent form is used: when A and B are jointly unsatisfiable, an interpolant is implied by A, inconsistent with B, and mentions only shared variables. For propositional logic one can be read off a resolution refutation in linear time.

In the refutation form, for $A\wedge B$ unsatisfiable, an interpolant $I$ satisfies

Craig proved existence for first-order logic in 1957.^[1] In the propositional case there are two explicit ones. Quantifying away the variables that occur only in $A$ gives the strongest interpolant, $\exists \bar{a}.A$, and quantifying away those only in $B$ gives the weakest, $\forall \bar{b}.\neg B$. Both can be exponentially large, so in practice interpolants are computed from proofs.

McMillan's system labels each clause $C$ of a resolution refutation of $A\wedge B$ with a partial interpolant $I(C)$:^[3]

where $C{|}_B$ is the disjunction of the literals of $C$ whose variables occur in $B$. The label of the empty clause is an interpolant, found in one pass over the proof and linear in its size.

Take $A=a\wedge (\neg a\vee b)$ and $B=(\neg b\vee c)\wedge \neg c$, which share only $b$:

clause      from            label
a           A               false        a does not occur in B
~a | b      A               b
b           resolve on a    false | b    a occurs only in A
~b | c      B               true
~c          B               true
~b          resolve on c    true & true  c occurs in B
(empty)     resolve on b    b & true     b is shared

The interpolant is $b$: $A$ implies it, it contradicts $B$, and it is the only variable they share.

In model checking, $A$ encodes the initial states and the first transition, and $B$ the remaining transitions up to a bad state. When the bounded check is unsatisfiable, the interpolant over-approximates the states reachable in one step while still excluding every path to a bad state. Replacing the initial states by it and repeating either reaches a fixed point, which is an inductive invariant proving the property, or produces a real counterexample when the bound is increased. SMT solvers compute interpolants for theories the same way, from their refutations.

• SATThe Boolean satisfiability problem: given a propositional formula, decide whether some assignment of true and false to its variables makes it true. It is the canonical NP-complete problem, and also one that modern solvers routinely settle for instances with millions of variables.
• CDCLConflict-driven clause learning: DPLL plus the observation that a conflict is a proof that some set of decisions is impossible. The solver analyses the implication graph, derives a new clause ruling that set out, adds it to the database, and backjumps possibly many levels at once rather than undoing one decision at a time.
• First-UIP conflict analysisThe procedure that turns a conflict into a learned clause. Walk the implication graph backwards from the conflicting clause, resolving away literals assigned at the current decision level until exactly one remains: that unique implication point gives the clause that is both strong and cheap to derive, and its second-highest level says how far to backjump.
• SMTSatisfiability modulo theories: SAT where the atoms are not opaque booleans but statements in some theory, such as linear arithmetic or equality over uninterpreted functions. The formula must be satisfiable both propositionally and in the theory, which is what makes SMT the engine under most program verifiers.
• ResolutionThe inference rule that combines two clauses containing a complementary pair of literals into one clause without them. It is refutation complete for propositional logic: a set of clauses is unsatisfiable exactly when the empty clause can be derived. DPLL runs correspond to tree-like resolution proofs, and CDCL runs to general ones.

1. [1]W. Craig, “Linear reasoning. A new form of the Herbrand–Gentzen theorem”, Journal of Symbolic Logic 22 (1957).
2. [2]P. Pudlák, “Lower bounds for resolution and cutting plane proofs and monotone computations”, Journal of Symbolic Logic 62 (1997).
3. [3]K. L. McMillan, “Interpolation and SAT-based model checking”, CAV (2003).