For a pair of inconsistent formulas , i.e., or **unsatisfiable**, the **Craig Interpolant** [1] 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 [2] 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 [3].

## 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 [4]. 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 .

#### References

- 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.