For a pair of inconsistent formulas , i.e., or unsatisfiable, the Craig Interpolant  for is a formula such that
- , and
- contains variables common to and .
The interpolant can be viewed as the part of that is sufficient, or relevant, to contradict . Modern SAT solvers produce a proof of unsatisfiability, or resolution proof, if the checked formula is unsatisfiable. An interpolant can be extracted in linear time  from a proof of unsatisfiability. The chief advantage of deriving interpolants from proofs is that they capture facts which the SAT solver derived about in showing that is inconsistent with . Therefore, assuming that the prover ignores irrelevant facts and focuses on real ones, interpolation can be thought of as a way of filtering out irrelevant information from .
Interpolants from Proofs
Preliminaries. A literal is a Boolean variable or its negation. A clause is a disjunction of zero or more literals. A clause set is satisfiable if there exists a truth assignment to the Boolean variables that makes all clauses in the set true. Given two clauses and , the resolvent of and is the clause , assuming is non-tautological, and is the pivot variable. Similarly, and have resolvent , while and have no resolvent, since is tautological. Therefore, the resolvent of clauses and is a clause that is implied by , and , where is the pivot variable.
Proof of Unsatisfiability
A proof of unsatisfiability for a set of clauses is a directed acyclic graph , where is a set of clauses, and
- for every vertex , either
- , and is a root, or
- has exactly two predecessors, and , such that is their resolvent, and
- the empty clause is an unique leaf.
If a proof on unsatisfiability exists for a set of clauses, then the clause set is unsatisfiable. In the satisfiable case, a SAT solver produces a satisfying assignment, whereas in the unsatisfiable case, it can produce a proof on unsatisfiability. The Wikipedia article on Resolution, along with Propositional Resolution, is a good starting point on the use of resolution to check satisfiability of a set of clauses.
Example 1: Consider clause set , such that , , , and . The proof of unsatisfiability graph for is shown in Figure 1. is resolvent of clauses and , and is resolvent of and . Resolvent clauses and are resolve to the empty leaf clause. Therefore, is unsatisfiable.
Algorithm to find Interpolants
Suppose we are given a pair of clause set and a proof of unsatisfiability of . Some terminology:
- Global variable: a variable appearing in both and .
- Local variable: a variable appearing only in .
Similarly, a literal is global or local to depending on the variable it contains. Given a clause , denotes the disjunction of the global literals in , and denotes the disjunction of local literals in with respect to .
Example 2: We have two clauses, and , and suppose and . Then
- , and
Algorithm: The description of the algorithm to find interpolant from proofs is based on . Let be a pair of set clauses and be the proof of unsatisfiability graph for inconsistency of . For every vertex , we compute a boolean formula as follows.
if c is root, i.e. c ∈ V then if c ∈ A then p(c) = g(c) else p(c) = True else a, b = predecessors of c v = pivot variable of a, b if v is local to A then p(c) = p(a) ∨ p(b) else p(c) = p(a) ∧ p(b)
The interpolant of is , where is leaf vertex in , or . The interpolant for is not unique and depends on the proof of unsatisfiability . Therefore, we often denote interpolant for with respect to as .
Complexity: Let be the number of vertices in , i.e., , and be the number of literals appearing in , i.e., . It the worst case, lines 2–5 repeat $N$ times, and lines 7–8 repeat since every literal in can be a pivot variable. Therefore, the formula can be computed in time, i.e., linear in the size of .
Example 4: Consider the clause set , such that , , , and , from Example 1. The proof of unsatisfiability for is shown in Figure 1. Let and . We know that is unsatisfiable. we first find the global and local literals for each clause in : , , , , , , , . Figure 2 shows the formulas computed using the above algorithm for every vertex of Figure 1.
For the leaf vertex , . Therefore, . It can be verified that is the interpolant of clause sets since , , and contains variables common to both and .
- K L McMillan. 2005. Applications of Craig Interpolants in Model Checking. In 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 1–12.
- K L McMillan. 2003. Interpolation and SAT-Based Model Checking. In 15th International Conference on Computer Aided Verification (CAV), 1–13.
- Pavel Pudlák. 1997. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic 62, 3 (1997), 981–998.
- William Craig. 1957. Linear reasoning. A new form of the Herbrand-Gentzen theorem. The Journal of Symbolic Logic 22, 3 (1957), 250–268.