cnf_satisfiable_append_sum_iff

theoremverified

Let f be a CNF formula over a variable type V and g a CNF formula over a variable type W. Replace every literal of f by the literal of the same sign whose variable is Sum.inl of the old variable, and every literal of g by the literal of the same sign whose variable is Sum.inr of the old variable, and concatenate the clause lists. The resulting formula over the disjoint union V ⊕ W is satisfiable if and only if f is satisfiable over V and g is satisfiable over W.

Statement

theorem cnf_satisfiable_append_sum_iff {V W : Type*} (f : List (List (CnfLit V)))
    (g : List (List (CnfLit W))) :
    CnfSatisfiable (f.map (List.map (fun l : CnfLit V =>
        match l with | CnfLit.pos v => CnfLit.pos (Sum.inl v) | CnfLit.neg v => CnfLit.neg (Sum.inl v)))
      ++ g.map (List.map (fun l : CnfLit W =>
        match l with | CnfLit.pos v => CnfLit.pos (Sum.inr v) | CnfLit.neg v => CnfLit.neg (Sum.inr v))))
      ↔ CnfSatisfiable f ∧ CnfSatisfiable g

Source

folklore; the gadget-composition step of the Cook-Levin theorem and of SAT ≤ 3SAT (Sipser, ch. 7; Garey & Johnson, ch. 3)

Verified

10 Sep 2026

Axioms

Quot.soundpropext

Built on 3

CnfSatisfiableA CNF formula (a list of clauses, each a list of literals) is satisfiable if there is a truth assignment such that every clause contains…
cnf_satisfiable_of_appendIf the concatenation `f1 ++ f2` of two CNF formulas is satisfiable (`CnfSatisfiable (f1 ++ f2)`), then both `f1` and `f2` are satisfiable…
CnfLitA CNF literal over a variable type V is either a positive variable or a negated variable.

Read back from the Lean

For all types V and W, and for all CNF formulas f over variable type V and g over variable type W (both represented as lists of clauses, each clause a list of CnfLit literals), the following equivalence holds: Take f and relabel every literal of f by tagging its variable with Sum.inl (i.e. put it on the left side of the disjoint sum V ⊕ W). Take g and relabel every literal of g by tagging its variable with Sum.inr (i.e. put it on the right side). Concatenate the two resulting lists of clauses. The resulting CNF formula is satisfiable if and only if f is satisfiable and g is satisfiable. Here “f is satisfiable” means, unfolding CnfSatisfiable, that there exists a Boolean assignment τ : V → Bool such that for every clause c in f there exists a literal l in c that τ makes true: CnfLit.pos v requires τ v = true, and CnfLit.neg v requires τ v = false. The analogous definition is used for g over W and for the combined formula over V ⊕ W. No hypotheses other than the type parameters V, W and the two explicit lists f, g are present: in particular, there are no Fintype or decidability assumptions, and f and g are arbitrary lists of clauses (including possibly empty lists and possibly empty clauses).

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

def cnf_satisfiable_append_sum_iff_lift_inl {V W : Type*} (l : CnfLit V) : CnfLit (V ⊕ W) :=
  match l with
  | CnfLit.pos v => CnfLit.pos (Sum.inl v)
  | CnfLit.neg v => CnfLit.neg (Sum.inl v)

def cnf_satisfiable_append_sum_iff_lift_inr {V W : Type*} (l : CnfLit W) : CnfLit (V ⊕ W) :=
  match l with
  | CnfLit.pos v => CnfLit.pos (Sum.inr v)
  | CnfLit.neg v => CnfLit.neg (Sum.inr v)

/-- Standardizing apart: clauses over disjoint variable sets are satisfiable jointly iff each is satisfiable separately. -/
theorem cnf_satisfiable_append_sum_iff {V W : Type*} (f : List (List (CnfLit V)))
    (g : List (List (CnfLit W))) :
    CnfSatisfiable (f.map (List.map (fun l : CnfLit V =>
        match l with | CnfLit.pos v => CnfLit.pos (Sum.inl v) | CnfLit.neg v => CnfLit.neg (Sum.inl v)))
      ++ g.map (List.map (fun l : CnfLit W =>
        match l with | CnfLit.pos v => CnfLit.pos (Sum.inr v) | CnfLit.neg v => CnfLit.neg (Sum.inr v))))
      ↔ CnfSatisfiable f ∧ CnfSatisfiable g := by
  change CnfSatisfiable (f.map (List.map (cnf_satisfiable_append_sum_iff_lift_inl (W := W)))
      ++ g.map (List.map (cnf_satisfiable_append_sum_iff_lift_inr (V := V))))
      ↔ CnfSatisfiable f ∧ CnfSatisfiable g
  constructor
  · intro h
    have hsplit := cnf_satisfiable_of_append h
    constructor
    · obtain ⟨ρ, hρ⟩ := hsplit.1
      refine ⟨fun v => ρ (Sum.inl v), ?_⟩
      intro c hc
      obtain ⟨l, hl, he⟩ := hρ (c.map (cnf_satisfiable_append_sum_iff_lift_inl (W := W))) (List.mem_map_of_mem hc)
      obtain ⟨l', hl', rfl⟩ := List.mem_map.mp hl
      cases l' with
      | pos v => exact ⟨CnfLit.pos v, hl', he⟩
      | neg v => exact ⟨CnfLit.neg v, hl', he⟩
    · obtain ⟨ρ, hρ⟩ := hsplit.2
      refine ⟨fun w => ρ (Sum.inr w), ?_⟩
      intro c hc
      obtain ⟨l, hl, he⟩ := hρ (c.map (cnf_satisfiable_append_sum_iff_lift_inr (V := V))) (List.mem_map_of_mem hc)
      obtain ⟨l', hl', rfl⟩ := List.mem_map.mp hl
      cases l' with
      | pos v => exact ⟨CnfLit.pos v, hl', he⟩
      | neg v => exact ⟨CnfLit.neg v, hl', he⟩
  · rintro ⟨⟨σ, hσ⟩, ⟨τ, hτ⟩⟩
    refine ⟨Sum.elim σ τ, ?_⟩
    intro c hc
    rw [List.mem_append] at hc
    rcases hc with hc | hc
    · obtain ⟨c', hc', rfl⟩ := List.mem_map.mp hc
      obtain ⟨l', hl', he⟩ := hσ c' hc'
      cases l' with
      | pos v => exact ⟨CnfLit.pos (Sum.inl v), List.mem_map_of_mem hl', he⟩
      | neg v => exact ⟨CnfLit.neg (Sum.inl v), List.mem_map_of_mem hl', he⟩
    · obtain ⟨c', hc', rfl⟩ := List.mem_map.mp hc
      obtain ⟨l', hl', he⟩ := hτ c' hc'
      cases l' with
      | pos v => exact ⟨CnfLit.pos (Sum.inr v), List.mem_map_of_mem hl', he⟩
      | neg v => exact ⟨CnfLit.neg (Sum.inr v), List.mem_map_of_mem hl', he⟩

Discuss this result Challenge it