cnf_satisfiable_subset
theoremverified
If every clause of a CNF formula `f1` is contained in a CNF formula `f2` (that is, `f1 ⊆ f2`), and `f2` is satisfiable (`CnfSatisfiable f2`), then `f1` is also satisfiable (`CnfSatisfiable f1`).
Statement
theorem cnf_satisfiable_subset {V : Type*} {f1 f2 : List (List (CnfLit V))} (hsub : f1 ⊆ f2) (hsat : CnfSatisfiable f2) : CnfSatisfiable f1
- Source
- Arora & Barak, Computational Complexity, Section 2.1
- Verified
- 07 Sep 2026
- Axioms
- none — Lean reports it depends on no axioms
- Built on 2
- 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…
- CnfLitA CNF literal over a variable type V is either a positive variable or a negated variable.
- Used by 1
- cnf_satisfiable_of_appendIf the concatenation `f1 ++ f2` of two CNF formulas is satisfiable (`CnfSatisfiable (f1 ++ f2)`), then both `f1` and `f2` are satisfiable…
Read back from the Lean
For any type V and any two CNF formulas f1 and f2 (represented as lists of lists of literals over V), if f1 is a sub-collection of f2 (every clause in f1 appears in f2), and f2 is CNF-satisfiable, then f1 is also CNF-satisfiable.
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
/-- Subformula monotonicity: any subformula (subset of clauses) of a satisfiable CNF formula is satisfiable. -/ theorem cnf_satisfiable_subset {V : Type*} {f1 f2 : List (List (CnfLit V))} (hsub : f1 ⊆ f2) (hsat : CnfSatisfiable f2) : CnfSatisfiable f1 := by obtain ⟨τ, hτ⟩ := hsat exact ⟨τ, fun c hc => hτ c (hsub hc)⟩