Craig interpolation

Craig's interpolation theorem, proved by William Craig in 1957, says that whenever a formula $A$ logically implies a formula $B$ , there is a formula $I$ such that $A$ implies $I$ , $I$ implies $B$ , and every non-logical symbol of $I$ occurs in both $A$ and $B$ ^[1]. The interpolant is an explanation of the implication in the shared vocabulary: it captures exactly what $A$ has to say that $B$ needs. The theorem holds for first-order and propositional logic. Its computational form made it a tool of automated verification: from a resolution refutation of an unsatisfiable conjunction $A \land B$ , an interpolant can be read off in one pass^[2]^[3]. Kenneth McMillan used such interpolants in 2003 to turn bounded model checking with a SAT solver into a complete method for proving safety properties^[3].

§ 01

Statement

In the refutation form used in automated reasoning, for $A \land B$ unsatisfiable, an interpolant $I$ satisfies

A ⊨ I, I \land B ⊨ ⊥, vars (I) \subseteq vars (A) \cap vars (B)

This is the original statement applied to $A ⊨ \neg B$ . In propositional logic, interpolants always exist and there are two extreme ones. Quantifying away the variables that occur only in $A$ gives the strongest interpolant, $\exists a ˉ . A$ , and quantifying away those that occur only in $B$ from $\neg B$ gives the weakest, $\forall b ˉ . \neg B$ . Every interpolant lies between them. Both can be exponentially large, and computing them requires eliminating quantifiers.

In the example below, a occurs only in A, c only in B, and b in both. An interpolant may mention only b.

§ 02

Interpolants from resolution proofs

Given a resolution refutation of $A \land B$ , each clause $C$ of the refutation can be labelled with a partial interpolant $I (C)$ . McMillan's system is^[3]:

I (C) = ⎩ ⎨ ⎧ C ∣_{B} ⊤ I (C_{1}) \lor I (C_{2}) I (C_{1}) \land I (C_{2}) C \in A C \in B p only in A otherwise

where the last two cases are for a resolvent $C$ of $C_{1}$ and $C_{2}$ on the pivot $p$ , and $C ∣_{B}$ is the disjunction of the literals of $C$ whose variables occur in $B$ . By induction over the proof, each label satisfies $A ⊨ I (C)$ and $I (C) \land B ⊨ C ∣_{B}$ , a clause restricted to shared literals, so the label of the empty clause is an interpolant. The computation is linear in the size of the proof, and the interpolant, viewed as a circuit with shared subterms, is as well. Pudlák's earlier system is symmetric between $A$ and $B$ ^[2]^[10]; D'Silva and co-authors showed that these systems are instances of a family that yields interpolants of different logical strength from the same proof^[5].

McMillan's labelling over the refutations produced by a small DPLL-based prover.

open Resproof
 
(* Interpolants as formulas, simplified as they are built. *)
type f = T | F | Lit of int | And of f * f | Or of f * f
let conj a b = match a, b with F, _ | _, F -> F | T, x | x, T -> x | _ -> if a = b then a else And (a, b)
let disj a b = match a, b with T, _ | _, T -> T | F, x | x, F -> x | _ -> if a = b then a else Or (a, b)
let rec eval env = function
  | T -> true | F -> false | Lit l -> if l > 0 then env l else not (env (-l))
  | And (a, b) -> eval env a && eval env b | Or (a, b) -> eval env a || eval env b
let rec vars = function T | F -> [] | Lit l -> [ abs l ] | And (a, b) | Or (a, b) -> vars a @ vars b
 
(* McMillan's labelling of a refutation of A ∧ B. Input clauses with
   index below na belong to A. *)
let interpolant ~na (a_vars : int list) (b_vars : int list) (p : proof) =
  let a_local v = List.mem v a_vars && not (List.mem v b_vars) in
  let rec label p =
    match p.step with
    | Input i when i < na ->                     (* A clause: its B-literals, disjoined *)
      List.fold_left (fun acc l -> if List.mem (abs l) b_vars then disj acc (Lit l) else acc) F p.clause
    | Input _ -> T                               (* B clause *)
    | Resolve (v, p1, p2) ->
      if a_local v then disj (label p1) (label p2) else conj (label p1) (label p2)
  in
  label p
 
let rec show_with name = function
  | T -> "⊤" | F -> "⊥"
  | Lit l -> (if l < 0 then "¬" else "") ^ name (abs l)
  | And (a, b) -> "(" ^ show_with name a ^ " ∧ " ^ show_with name b ^ ")"
  | Or (a, b) -> "(" ^ show_with name a ^ " ∨ " ^ show_with name b ^ ")"
let show = show_with (fun v -> String.make 1 (Char.chr (Char.code 'a' + v - 1)))

The example of the figure.

open Interp

Running it.

refutation with 7 clauses
interpolant: b

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

Checking the construction on random unsatisfiable pairs by brute force.

open Interp
 
(* Random unsatisfiable pairs over variables 1-4 (A only), 5-7 (shared)
   and 8-11 (B only), checked by brute force over all assignments. *)
let clause pool = List.init 3 (fun _ ->
    let v = List.nth pool (Random.int (List.length pool)) in if Random.bool () then v else -v)
let sat_of cs env = List.for_all (List.exists (fun l -> if l > 0 then env l else not (env (-l)))) cs

Running it.

300 unsatisfiable pairs, 300 interpolants correct, average 8.0 literal occurrences

§ 03

Model checking

Bounded model checking unrolls a transition system $k$ steps and asks a SAT solver whether a bad state is reachable within those steps; it finds errors but cannot prove their absence. McMillan observed that when the bounded check fails, the refutation contains an over-approximation of the reachable states that is still too weak to reach a bad state^[3]. Split the unrolled formula into $A = R (s_{0}) \land T (s_{0}, s_{1})$ , the current approximation $R$ of the initial states and one transition, and $B$ , the remaining transitions and the bad states. The interpolant mentions only $s_{1}$ and describes a set of states that contains every successor of $R$ and from which no bad state is reachable in $k - 1$ steps. Adding it to $R$ and repeating either reaches a fixed point, an inductive invariant that proves the property, or finds that the enlarged $R$ reaches a bad state, in which case the check is repeated with a larger $k$ .

Interpolation-based model checking of a 3-bit counter that starts at 0 and adds 2: can it reach an odd value?

open Interp
 
(* A 3-bit counter that starts at 0 and adds 2 modulo 8. Is an odd state
   reachable? State bit j at time t is variable 3t + j + 1. *)
let bit t j = (3 * t) + j + 1
let trans t =                                  (* state t+1 = state t + 2 *)
  let x j = bit t j and y j = bit (t + 1) j in
  [ [ -y 0; x 0 ]; [ y 0; -x 0 ];                                 (* bit 0 unchanged *)
    [ -y 1; -x 1 ]; [ y 1; x 1 ];                                 (* bit 1 flips *)
    [ -y 2; x 2; x 1 ]; [ -y 2; -x 2; -x 1 ]; [ y 2; -x 2; x 1 ]; [ y 2; x 2; -x 1 ] ] (* bit 2 ^= bit 1 *)
 
(* A set of states over time 0, as clauses excluding every other state. *)
let states_at t set =
  List.filter_map (fun s -> if List.mem s set then None
                    else Some (List.init 3 (fun j -> if s land (1 lsl j) <> 0 then - (bit t j) else bit t j)))
    (List.init 8 Fun.id)
let states_of t f =
  List.filter (fun s -> eval (fun v -> let tt = (v - 1) / 3 and j = (v - 1) mod 3 in
                              tt = t && s land (1 lsl j) <> 0) f) (List.init 8 Fun.id)
let show_set s = "{" ^ String.concat "," (List.map string_of_int s) ^ "}"
 
(* McMillan's loop with k steps of lookahead: A is "R at time 0 and one
   step", B is "k - 1 more steps and an odd state at some time 1..k". *)
let check k =
  let rec loop r =
    let a = states_at 0 r @ trans 0 in
    let b = List.concat (List.init (k - 1) (fun t -> trans (t + 1)))
            @ [ List.init k (fun t -> bit (t + 1) 0) ] in
    let vars_of cs = List.sort_uniq compare (List.map abs (List.concat cs)) in
    match Resproof.refute (a @ b) with
    | None -> Printf.printf "  R = %s reaches a bad state within %d steps\n" (show_set r) k; `Unknown
    | Some p ->
      let i = interpolant ~na:(List.length a) (vars_of a) (vars_of b) p in
      let img = states_of 1 i in
      Printf.printf "  R = %-10s interpolant %s, the states %s\n" (show_set r)
        (show_with (fun v -> Printf.sprintf "s%d.bit%d" ((v - 1) / 3) ((v - 1) mod 3)) i) (show_set img);
      if List.for_all (fun s -> List.mem s r) img then `Safe r
      else loop (List.sort_uniq compare (r @ img))
  in
  loop [ 0 ]

Running it.

k = 1:
  R = {0}        interpolant ¬s1.bit0, the states {0,2,4,6}
  R = {0,2,4,6}  interpolant ¬s1.bit0, the states {0,2,4,6}
  fixed point: {0,2,4,6} is closed under a step and has no odd state
k = 3:
  R = {0}        interpolant ¬s1.bit0, the states {0,2,4,6}
  R = {0,2,4,6}  interpolant ¬s1.bit0, the states {0,2,4,6}
  fixed point: {0,2,4,6} is closed under a step and has no odd state

The first interpolant is not the exact image of ${0}$ , which is ${2}$ , but the more general statement that the lowest bit is 0. That generalization is what makes the method converge: after one step, the approximation ${0, 2, 4, 6}$ is closed under the transition and contains no odd state, so it is an invariant proving the property. Interpolants over theories, computed from SMT refutations, serve the same purpose in software model checking, where they supply the predicates for abstraction refinement^[6]^[7].

§ 04

Proof complexity

Because an interpolant can be computed from a resolution refutation as a circuit of linear size, lower bounds on circuits give lower bounds on proofs. This is feasible interpolation: Krajíček showed in 1997 that for resolution and several other proof systems, a refutation of size $S$ yields an interpolating circuit of size polynomial in $S$ , and when the shared variables occur only positively in $A$ , a monotone one^[4]. Pudlák applied it to cutting planes^[2]. Formulas whose interpolants must be large monotone circuits, such as those encoding the clique–colouring problem, therefore have no short refutations in these systems.

§ 05

History

Craig proved the theorem for first-order logic in 1957 as a consequence of Gentzen's cut elimination^[1]. Lyndon strengthened it in 1959 to preserve the polarity of predicate symbols^[8], and Beth's definability theorem of 1953 follows from it^[9]. Its use in proof complexity began with Krajíček and Pudlák in the 1990s^[4]^[2], and Huang, Krajíček and Pudlák independently gave the symmetric labelling of resolution proofs^[10]^[4]^[2]. McMillan's paper of 2003 made interpolation a mainstream verification technique^[3], followed by interpolating SMT solvers and interpolation-based abstraction refinement for software^[6]^[7].