Introduction

Every proof of contradiction carries a secret. In 1957, logician William Craig noticed that whenever two formulas AA and BB together are unsatisfiable — meaning no assignment of truth values can satisfy both at once — there is always a third formula II that:

  1. is implied by AA (every model of AA is also a model of II),
  2. is inconsistent with BB (I∧BI \land B is unsatisfiable),
  3. only mentions symbols that appear in both AA and BB.

That formula II is the interpolant. It speaks only the shared language of AA and BB, yet it fully explains the contradiction between them. Craig proved such an II always exists for classical propositional and first-order logic.

For half a century the theorem lived quietly in logic textbooks. Then, in 2003, Kenneth McMillan discovered that SAT solvers could compute interpolants from resolution proofs — and suddenly the theorem became the engine behind modern program verification.

Derive the Interpolant

Pick two propositional formulas AA and BB from the presets below, or enter your own. The demo checks that A∧BA \land B is unsatisfiable, then derives an interpolant II over the shared variables.

<!-- Craig Interpolation demo: A and B are entered, an interpolant I is derived -->
<div class="panel">
  <label class="label">Presets</label>
  <div class="presets" id="presets"></div>
</div>
<div class="panel two-col">
  <div>
    <label class="label">Formula A</label>
    <textarea id="inputA" rows="2" placeholder="e.g. p AND q"></textarea>
  </div>
  <div>
    <label class="label">Formula B</label>
    <textarea id="inputB" rows="2" placeholder="e.g. NOT p"></textarea>
  </div>
</div>
<button id="btnDerive" type="button">Derive interpolant</button>
<div id="status" class="status"></div>
<div id="result" class="result hidden">
  <div class="row"><span class="tag tagA">A</span><span id="dispA"></span></div>
  <div class="row"><span class="tag tagI">I</span><span id="dispI"></span></div>
  <div class="row"><span class="tag tagB">B</span><span id="dispB"></span></div>
  <div id="explanation" class="explanation"></div>
</div>

/* Styles for the Craig Interpolation demo */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.panel { margin-bottom: .75rem; }
.two-col { display: grid; grid-template-columns: 1fr 1fr; gap: .6rem; }
.label { display: block; font-size: .8rem; font-weight: 600; color: #555; margin-bottom: .25rem; text-transform: uppercase; letter-spacing: .04em; }
textarea { width: 100%; font: 14px ui-monospace, monospace; border: 1px solid #cdd9e3; border-radius: 6px; padding: .4rem .5rem; resize: vertical; }
textarea:focus { outline: 2px solid #1d3557; }
.presets { display: flex; flex-wrap: wrap; gap: .4rem; }
.preset-btn { font: 600 12px system-ui; padding: .3rem .7rem; border: 1px solid #1d3557; border-radius: 20px; background: #fff; color: #1d3557; cursor: pointer; transition: background .15s; }
.preset-btn:hover, .preset-btn.active { background: #1d3557; color: #fff; }
button#btnDerive { font: 600 14px system-ui; padding: .45rem 1.1rem; border: 1px solid #1d3557; background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; margin-bottom: .6rem; }
.status { font-size: .9rem; font-weight: 600; min-height: 1.4em; margin-bottom: .5rem; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
.result { background: #f6f8fb; border: 1px solid #cdd9e3; border-radius: 8px; padding: .75rem; }
.result.hidden { display: none; }
.row { display: flex; align-items: baseline; gap: .5rem; margin-bottom: .35rem; font: 14px ui-monospace, monospace; }
.tag { display: inline-block; width: 1.5rem; text-align: center; font: 700 12px system-ui; padding: .1rem 0; border-radius: 4px; }
.tagA { background: #dbeafe; color: #1e3a8a; }
.tagI { background: #d1fae5; color: #065f46; font-size: 13px; }
.tagB { background: #ffe4e6; color: #9b1c1c; }
.explanation { font-size: .82rem; color: #444; line-height: 1.5; margin-top: .5rem; border-top: 1px solid #dde3ea; padding-top: .5rem; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Craig Interpolation demo
// Approach: enumerate assignments to compute a DNF interpolant over the shared variables.

// Built-in preset examples (A, B pairs that are unsatisfiable together)
const PRESETS = [
  { label: 'A: p∧q | B: ¬p', a: 'p AND q', b: 'NOT p' },
  { label: 'A: (p∨q)∧r | B: ¬r', a: '(p OR q) AND r', b: 'NOT r' },
  { label: 'A: p∧q | B: ¬q', a: 'p AND q', b: 'NOT q' },
  { label: 'A: (p∨q)∧¬q | B: ¬p∧¬q', a: '(p OR q) AND NOT q', b: 'NOT p AND NOT q' }
];

// Tokenize: uppercase + split on parentheses and whitespace
function tokenize(s) {
  return s.toUpperCase()
    .replace(/\(/g,' ( ').replace(/\)/g,' ) ')
    .trim().split(/\s+/).filter(Boolean);
}

// Recursive-descent parser: handles AND, OR, NOT, IMPLIES, parentheses, variables
function parse(tokens, pos) {
  pos = pos || 0;
  let left, res;
  [left, pos] = parseAtom(tokens, pos);
  while (pos < tokens.length) {
    const t = tokens[pos];
    if (t === 'AND') {
      let right; [right, pos] = parseAtom(tokens, pos + 1);
      left = { op: 'and', l: left, r: right };
    } else if (t === 'OR') {
      let right; [right, pos] = parseAtom(tokens, pos + 1);
      left = { op: 'or', l: left, r: right };
    } else if (t === 'IMPLIES') {
      let right; [right, pos] = parseAtom(tokens, pos + 1);
      left = { op: 'or', l: { op: 'not', x: left }, r: right };
    } else { break; }
  }
  return [left, pos];
}

function parseAtom(tokens, pos) {
  if (tokens[pos] === 'NOT') {
    let inner; [inner, pos] = parseAtom(tokens, pos + 1);
    return [{ op: 'not', x: inner }, pos];
  }
  if (tokens[pos] === '(') {
    let inner; [inner, pos] = parse(tokens, pos + 1);
    if (tokens[pos] !== ')') throw new Error('Missing closing parenthesis');
    return [inner, pos + 1];
  }
  if (/^[A-Z][A-Z0-9_]*$/.test(tokens[pos])) return [{ op: 'var', v: tokens[pos] }, pos + 1];
  throw new Error(fmt('Unexpected token: %v%', { v: tokens[pos] }));
}

function parseFormula(s) {
  const toks = tokenize(s);
  const [ast, pos] = parse(toks, 0);
  if (pos !== toks.length) throw new Error('Unexpected tokens after formula');
  return ast;
}

// Evaluate an AST node under a variable assignment (env maps variable name to boolean)
function evalAST(node, env) {
  if (node.op === 'var') return !!env[node.v];
  if (node.op === 'not') return !evalAST(node.x, env);
  if (node.op === 'and') return evalAST(node.l, env) && evalAST(node.r, env);
  if (node.op === 'or')  return evalAST(node.l, env) || evalAST(node.r, env);
  return false;
}

// Collect all variable names in an AST
function getVars(node, out) {
  out = out || new Set();
  if (node.op === 'var') { out.add(node.v); return out; }
  if (node.x) getVars(node.x, out);
  if (node.l) getVars(node.l, out);
  if (node.r) getVars(node.r, out);
  return out;
}

// Enumerate all 2^n truth assignments for a list of variable names
function allAssignments(vars) {
  const n = vars.length, res = [];
  for (let mask = 0; mask < (1 << n); mask++) {
    const env = {};
    vars.forEach((v, i) => { env[v] = !!(mask & (1 << i)); });
    res.push(env);
  }
  return res;
}

// Derive a Craig interpolant I over the shared variables.
// I is the set of shared-variable assignments under which A has some satisfying extension.
function deriveInterpolant(astA, astB, sharedVars, allVars) {
  const shared = Array.from(sharedVars).sort();
  const sharedAssignments = allAssignments(shared);
  // For each shared-variable assignment, check if A can be satisfied given it
  const trueRows = [];
  for (const sEnv of sharedAssignments) {
    // Try to satisfy A with this shared assignment by trying all private-variable values
    const aVars = Array.from(getVars(astA));
    const aPrivate = aVars.filter(v => !sharedVars.has(v));
    const aAssigns = allAssignments(aPrivate);
    let aEntails = false;
    for (const aExt of aAssigns) {
      const env = Object.assign({}, sEnv, aExt);
      if (evalAST(astA, env)) { aEntails = true; break; }
    }
    if (aEntails) trueRows.push(Object.assign({}, sEnv));
  }
  // Build I as a DNF over the true shared-variable rows
  if (trueRows.length === 0) return 'FALSE';
  const clauses = trueRows.map(env =>
    shared.map(v => (env[v] ? v : 'NOT ' + v)).join(' AND ')
  );
  return clauses.map(c => shared.length > 1 ? '(' + c + ')' : c).join('\n  OR ');
}

function setStatus(msg, cls) {
  const el = document.getElementById('status');
  el.textContent = msg;
  el.className = 'status ' + (cls || '');
}

function derive() {
  const sA = document.getElementById('inputA').value.trim();
  const sB = document.getElementById('inputB').value.trim();
  document.getElementById('result').classList.add('hidden');
  if (!sA || !sB) { setStatus('Enter formulas for both A and B.', 'bad'); return; }

  let astA, astB;
  try { astA = parseFormula(sA); } catch(e) { setStatus(fmt('Parse error in A: %message%', { message: e.message }), 'bad'); return; }
  try { astB = parseFormula(sB); } catch(e) { setStatus(fmt('Parse error in B: %message%', { message: e.message }), 'bad'); return; }

  const varsA = getVars(astA);
  const varsB = getVars(astB);
  const allVarsSet = new Set([...varsA, ...varsB]);
  const allVars = Array.from(allVarsSet).sort();
  const sharedVars = new Set([...varsA].filter(v => varsB.has(v)));

  // Check that A AND B is indeed unsatisfiable
  let isSat = false;
  for (const env of allAssignments(allVars)) {
    if (evalAST(astA, env) && evalAST(astB, env)) { isSat = true; break; }
  }

  if (isSat) {
    setStatus('A ∧ B is satisfiable — no interpolant exists (they are compatible).', 'bad');
    return;
  }

  if (sharedVars.size === 0) {
    setStatus('A and B share no variables — interpolant would be TRUE or FALSE trivially.', 'bad');
    return;
  }

  const interpolant = deriveInterpolant(astA, astB, sharedVars, allVarsSet);

  // Verify the three Craig interpolation properties
  let interpAST;
  try { interpAST = parseFormula(interpolant.replace(/\n\s*/g, ' ')); } catch(e) {
    setStatus('Internal error computing interpolant.', 'bad'); return;
  }

  // Property 1: A implies I
  let aImpliesI = true;
  for (const env of allAssignments(allVars)) {
    if (evalAST(astA, env) && !evalAST(interpAST, env)) { aImpliesI = false; break; }
  }
  // Property 2: I AND B is unsatisfiable
  let iAndBUnsat = true;
  for (const env of allAssignments(allVars)) {
    if (evalAST(interpAST, env) && evalAST(astB, env)) { iAndBUnsat = false; break; }
  }

  const sharedList = Array.from(sharedVars).sort().join(', ');
  const onlyShared = (function() {
    const iv = getVars(interpAST);
    return [...iv].every(v => sharedVars.has(v));
  })();

  setStatus('✓ Interpolant derived successfully.', 'ok');
  document.getElementById('dispA').textContent = sA;
  document.getElementById('dispI').textContent = interpolant.replace(/\n\s*/g, ' ');
  document.getElementById('dispB').textContent = sB;
  const expl = document.getElementById('explanation');
  expl.innerHTML =
    fmt('<b>Shared variables:</b> %v%<br>%v2%<br>%v3%<br>%v4%', { v: sharedList || '—', v2: aImpliesI ? '✓ A ⊨ I  (every model of A satisfies I)' : '✗ A ⊭ I  (check failed)', v3: iAndBUnsat ? '✓ I ∧ B is unsatisfiable  (I blocks all models of B)' : '✗ I ∧ B is satisfiable  (check failed)', v4: onlyShared ? '✓ I mentions only shared symbols' : '✗ I contains non-shared symbols  (check failed)' });
  document.getElementById('result').classList.remove('hidden');
}

// Build preset buttons
const container = document.getElementById('presets');
PRESETS.forEach((p, i) => {
  const btn = document.createElement('button');
  btn.className = 'preset-btn';
  btn.textContent = p.label;
  btn.addEventListener('click', () => {
    document.getElementById('inputA').value = p.a;
    document.getElementById('inputB').value = p.b;
    document.querySelectorAll('.preset-btn').forEach(b => b.classList.remove('active'));
    btn.classList.add('active');
    derive();
  });
  container.appendChild(btn);
});
document.getElementById('btnDerive').addEventListener('click', derive);
// Load first preset on startup
document.getElementById('inputA').value = PRESETS[0].a;
document.getElementById('inputB').value = PRESETS[0].b;
container.children[0].classList.add('active');
derive();
Result
Console

Notice the key property: II only mentions variables that appear in both AA and BB. Variables private to AA vanish; variables private to BB also vanish. What remains is the exact shared reason the two sides cannot agree.

The Real Complexity

Craig's theorem guarantees existence but says nothing about size. In practice:

  • Computing an interpolant from a resolution proof runs in polynomial time in the proof size — each resolution step contributes at most a small formula fragment.
  • The result can be exponentially large as a formula. A compact proof can still produce an interpolant with exponentially many clauses when written in CNF.
  • Circuits save the day. Representing the interpolant as a Boolean circuit (DAG) keeps it polynomial in the proof size. McMillan's 2003 key insight was to stay in circuit form and never expand to CNF.
  • Minimal interpolants are hard. Finding the smallest formula that separates AA from BB is Σ2P\Sigma_2^P-complete — one level above NP in the polynomial hierarchy.

The gap between "interpolants exist and are easy to compute" and "the smallest interpolant is hard to find" mirrors a recurring theme in logic: existence is cheap, optimality is expensive.

Where It Matters

Craig interpolation turned from a curiosity into a cornerstone of automated reasoning:

  • CEGAR (Counterexample-Guided Abstraction Refinement): when a model checker finds a spurious counterexample, it uses interpolation to extract an invariant that rules it out and refine the abstraction. Tools like SLAM and Blast use this to verify millions of lines of code automatically.
  • Invariant synthesis: the interpolant between the initial states AA and the bad states BB is often exactly the inductive invariant a proof needs. The formula says "this is what always holds between the two sides."
  • Modular reasoning: interpolants let you summarize what one module "tells" another without exposing internal variables — the shared symbols become a clean interface specification.
  • Interpolating theorem provers: tools like iZ3 and SMTInterpol extend Craig interpolation to richer theories (integers, arrays, uninterpreted functions) used in real programs.

Understanding Craig interpolation means understanding why SAT-based verification can scale to real software — it is the mechanism that turns a proof of failure into a formula that prevents the same failure from recurring.

Conclusion

Craig interpolation is one of logic's quiet triumphs: a theorem proved for purely philosophical reasons in 1957 that turned out to be exactly the tool verification engineers needed half a century later.

The interpolant II that sits between AA and BB is not just any separator — it is the minimal shared explanation of their conflict, speaking only the language both sides understand. Extracting it from a resolution proof is cheap; using it to synthesize invariants and refine abstractions made automated verification of real software possible.

The next time a SAT solver tells you a system is correct, there is a good chance a Craig interpolant is the reason it could figure that out at all.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/craig-interpolation/Content licensed under CC BY-NC 4.0.