CnfSatisfiable

A CNF formula (a list of clauses, each a list of literals) is satisfiable if there is a truth assignment such that every clause contains at least one true literal.

Statement

def CnfSatisfiable {V : Type*} (f : List (List (CnfLit V))) : Prop

Verified

06 Sep 2026

Axioms

none listed

Built on 1

• CnfLitA CNF literal over a variable type V is either a positive variable or a negated variable.

Used by 5

• cnf_satisfiable_append_sum_iffLet 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…
• cnf_satisfiable_subsetIf every clause of a CNF formula `f1` is contained in a CNF formula `f2` (that is, `f1 ⊆ f2`), and `f2` is satisfiable (`CnfSatisfiable…
• cnf_single_clause_satisfiable_iffA CNF formula consisting of a single clause `c`, namely `[c]`, is satisfiable (`CnfSatisfiable [c]`) if and only if the clause `c` is…
• cnf_satisfiable_of_appendIf the concatenation `f1 ++ f2` of two CNF formulas is satisfiable (`CnfSatisfiable (f1 ++ f2)`), then both `f1` and `f2` are satisfiable…
• cnf_empty_satisfiableThe empty CNF formula has no clauses to satisfy, hence is satisfiable under any truth assignment.

Lean source view module on GitHub

/-- A CNF formula is satisfiable if there exists a truth assignment satisfying at least one literal in each clause. -/
def CnfSatisfiable {V : Type*} (f : List (List (CnfLit V))) : Prop := ∃ τ : V → Bool, ∀ c ∈ f, ∃ l ∈ c, match l with
    | CnfLit.pos v => τ v = true
    | CnfLit.neg v => τ v = false