Interpolants and Relevance

  • logic
  • interpolants

» This post is a part of a series on ideas from symbolic logic lifted to verification «


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.

Figure 1: A proof of unsatisfiability graph for clauses , , , and .

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.

Figure 2: Intermediate formulas for every vertex in the proof of unsatisfiability graph 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

  1. 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.
  2. K L McMillan. 2003. Interpolation and SAT-Based Model Checking. In 15th International Conference on Computer Aided Verification (CAV), 1–13.
  3. 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.
  4. William Craig. 1957. Linear reasoning. A new form of the Herbrand-Gentzen theorem. The Journal of Symbolic Logic 22, 3 (1957), 250–268.