Conjunctive normal form

AbbreviationCNF clause#✓fully proved

A CNF clause is a finite list of literals, each a pair \((x, b)\) of a variable index \(x \in \mathbb{N}\) and a polarity \(b \in \{\mathrm{true}, \mathrm{false}\}\).

abbrev CNFClause := List (Nat × Bool)

Used by 289

AbbreviationCNF formula#✓fully proved

A CNF formula is a finite list of CNF clauses, read as the conjunction of its clauses.

abbrev CNF := List CNFClause

Uses 1 · Used by 329

Statement usesCNF clause

Used byRandom 3-SAT satisfiability agrees with CNF satisfiability · CNF formula of a random 3-SAT formula · Adjacency table of the implication graph · 2-SAT characterization · SCC-based 2-SAT decision procedure · Correctness of the SCC-based 2-SAT procedure · Resolution refutations give contradictory cycles · Implication edge · Reachability in the implication graph · Implication graph as a finite directed graph · Reachability in the finite implication graph · Resolution invariant of the implication graph · 2-CNF formulas · Literals over the variables of a formula · List of the literals of a CNF formula · Implication edges end over variables of the formula · A positive literal reaching its complement lies over a variable of the formula · Complement of a literal over a formula · Satisfying assignments respect implication edges · Skew symmetry of the implication graph · Successors in the implication graph · Duplicate-free list of the variables of a CNF formula · Restriction reduces the number of variables · Accumulating CNF builder · CNF of a proposition at a polarity · Disjoining CNF builder · Satisfiability means having a satisfying assignment · Satisfiability of a CNF with falsum false · Satisfiability of a CNF formula · Disjunction of two CNFs · The restricted variable no longer occurs · Restriction of a CNF formula by a literal · Unit propagation preserves satisfiability · Splitting on a variable · Satisfaction of a CNF formula · Satisfaction depends only on the occurring variables · Lifting a satisfying assignment from a restriction · Satisfaction of a restricted CNF formula · Equivalent CNF · CNF of a proposition · CNF of the complement of a proposition · Variables of a CNF formula · Restricting by an occurring variable shrinks the variable set · Restriction does not add variables · Davis-Putnam elimination preserves satisfiability · The Davis-Putnam procedure · Correctness of the Davis-Putnam procedure · Davis-Putnam elimination of a variable · Successive elimination of a list of variables · Completeness of a Davis-Putnam step · Clauses containing a variable only negatively · Clauses containing a variable only positively · Soundness of a Davis-Putnam step · Variable list for Davis–Putnam elimination · DPLL with a fuel budget · The DPLL procedure · First unit literal · First variable of a CNF formula · Boolean formula satisfaction check · Correctness of DPLL with sufficient fuel · Correctness of DPLL · Forward-chaining closure · Forward-chaining step · Horn satisfiability test · Correctness of the Horn satisfiability test · Horn formula · Least model candidate · On Horn formulas, the least model candidate lies below every model · Horn satisfiability via the least model · Compaction preserves clause-length bounds · Counting satisfying assignments over a larger variable range · Compaction preserves clause lengths · Exact variable compaction of a CNF formula · Unique satisfying extension in the parsimonious 3-CNF reduction · The parsimonious reduction outputs a duplicate-free 3-CNF · Compaction preserves the number of clauses · Model count of a CNF formula · Variable compaction preserves the model count · The parsimonious 3-CNF reduction preserves the model count · Compaction preserves absence of duplicate clauses · Number of fresh variables in the parsimonious 3-CNF reduction · Satisfaction is preserved by variable compaction · Soundness of the parsimonious 3-CNF reduction · Size bounds for the parsimonious 3-CNF reduction · Parsimonious reduction of CNF to 3-CNF · Variables of a compacted formula form an initial range · Lifting lemma · Clauses of a restricted formula · Unsatisfiable formulas without variables contain the empty clause · Refutable formulas are unsatisfiable · Resolution derivability · Soundness and refutation completeness · Refutation completeness · Soundness of resolution · One step of the linear-time Tseitin builder · Tseitin clauses for a conjunction · Equisatisfiability of the Tseitin transformation · Tseitin correctness · Tseitin clauses for an implication · Tseitin clauses have at most three literals · Number of clauses of the Tseitin CNF · Number of defining clauses in the Tseitin encoding · Tseitin clauses for a disjunction · Satisfying a concatenation of CNF formulas · Satisfaction depends only on the occurring variables · Tseitin encoding invariant · Correctness invariant of the Tseitin encoding · Tseitin CNF · Linear-time Tseitin builder · The linear-time Tseitin builder agrees with the reference encoding · Tseitin encoding with gates numbered from \(k\) · Tseitin CNF with \(\bot\) false · The Tseitin CNF reorders the reference encoding · One step of the Tseitin encoding · Evaluation of a quantified CNF formula · TQBF as a decision problem · UNSAT as a decision problem · Preimage of SAT under a polynomial-time map is in NP · Counting satisfying assignments of a CNF formula · The MAJSAT language · CNF encoding of a word-equation system at fixed lengths · CNF encoding uses clauses of width at most two · Fixed-length bit-blasting is equisatisfiable · Position-wise equality clauses for literal vectors · Clauses for a word equation with a length check · Clause count for one word equation · Clauses forcing two literals to be equal · SAT iff the bounded-search specification holds of the encoding · Correctness of the SAT-to-string-constraints translation · Encoding of CNF formulas as string constraints · Decoding a fixed number of clauses · Decoding a complete length-prefixed CNF formula · The CNF decoder inverts the length-prefixed CNF code · Decoding a length-prefixed CNF formula · Length-prefixed binary code of a CNF formula · Encodings of satisfiable CNF formulas · Binary-index translation of a dense formula · The binary-index translation preserves satisfiability when all clauses have equal length · The translation computes the binary encoding · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · Every NP problem reduces to binary-index CNF-SAT · Formula check against a witness · Correctness of the witness formula check · Cost bound for the witness formula check · Variables of a formula occur in its occurrence list · The SAT verifier · The SAT verifier rejects undecodable inputs · The SAT verifier on a decodable input · Declared time bound of the SAT verifier · The SAT verifier verifies SAT · The literal count is at most the code length · Occurrence list of a CNF formula · Length of the occurrence list · Clause check against an occurrence table · The clause check on the occurrence table is the formula check · Occurrence table of a formula and a witness · The SAT verifier's answer through the occurrence table · Tokenizer of the SAT verifier · Token sequence of a CNF formula · Clause loop of the clause check · The clause check · Token count is bounded by the encoding length · Tokenizer rejects undecodable clauses · Tokenizer run on all clauses · Rejecting run · Accepting run of the SAT tokenizer · Answer of the SAT host · Driver stacks after tokenization · The SAT verifier is polynomial-time · The TM2 SAT verifier · Answer of the SAT host with the three-literal filter · 3SAT is in NP · Token length bound for the SAT verifier (moved alias) · The SAT-to-3-COLOR graph construction · The SAT to 3-COLOR reduction map on bit strings · The 3-COLOR instance of a CNF formula · Correctness of the reduction from SAT to 3-coloring · The construction's edges lie below its vertex count · Correctness of the SAT to 3-COLOR map on bit strings · The emitter on a list of clauses · Correctness and step bound of the 3-COLOR emitter · The 3-COLOR emitter · The SAT-to-3-COLOR reduction is polynomial-time · Adjacency bits of Karp's clique graph · Literal occurrences of a CNF formula · Karp's SAT-to-CLIQUE map on bit strings · Karp's CLIQUE instance of a CNF formula · Karp's reduction from SAT to CLIQUE is correct · Membership in the literal occurrences of a CNF formula · SAT decision on undecodable input (moved alias) · Adjacency in Karp's clique graph · Pair bits of a leading clause · Walked items of a formula · Occurrences of a formula with a first clause · Row bits of a formula for the CLIQUE emitter · The CLIQUE emitter's row bits are Karp's pair bits · Clique emitter: one clause · Emitter run over a formula's clauses · The CLIQUE emitter computes Karp's instance in cubic time · The CLIQUE emitter · SAT ≤ CLIQUE is polynomial-time · CLIQUE is NP-hard · Normal clause detours · Arcs of a variable diamond · Arcs of the HAMPATH construction · Distinct variables of a formula · The SAT-to-HAMPATH reduction map · Sipser's HAMPATH instance of a CNF formula · Hamiltonian paths of Sipser's graph have normal detours · Classification of the arcs of Sipser's graph · Out-neighbours of a clause vertex in Sipser's graph · Out-neighbours of a row vertex in Sipser's graph · Consecutive vertices of a Hamiltonian path of Sipser's graph form arcs · In-neighbours of a clause vertex in Sipser's graph · In-neighbours of a row vertex in Sipser's graph · A clause detour returns to its own pair (Sipser's separator argument) · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A separator is next to each of its row neighbours on a Hamiltonian path · Arcs of the Hamiltonian path construction · The HAMPATH instance as unary blocks and arc bits · Splitting off the middle clause of a concatenation · HAMPATH emitter, phase A: the clauses of a formula · The emitter state before the diamonds · The detour walk of a diamond in the HAMPATH emitter · Initial state of the HAMPATH emitter · Phase A of the HAMPATH emitter · End of a diamond · The detours of a diamond · One diamond · The diamonds · Correctness and running time of the HAMPATH emitter · In-neighbours of a row vertex outside the clause vertices · Consecutive vertices of the contracted path are joined by arcs · Deleting the clause vertices from a path · Satisfiable formulas give Hamiltonian paths (SAT ≤ HAMPATH, forward direction) · Arcs from a row into a clause vertex · Out-neighbours of a row vertex outside the clause vertices · Out-neighbours of a top · Contracting a clause detour · A satisfying choice gives a Hamiltonian path · The frame arcs of a diamond · The detour arcs of a negative occurrence · Positive detour arcs of a diamond · Row arcs of a diamond · Diamond arcs are arcs of the construction · Backward direction of SAT ≤ HAMPATH for paths with normal detours · Every vertex of the contracted path except its end has a successor · The construction has a Hamiltonian path iff the formula is satisfiable · Every top but the last is followed by an end of its row · Positions in the list of distinct variables · Entering a row and leaving it at once is impossible · A row entered at one end is run to the other end · SAT ≤ HAMPATH preserves membership · The HAMPATH emitter · SAT ≤ HAMPATH is polynomial-time · The 1-in-3-SAT decision problem · Feasible 1-in-3-SAT instances · 1-in-3-SAT instances · Well-formed 1-in-3-SAT instances · 3-SAT with bounded occurrences as a decision problem · Satisfiable bounded-occurrence 3-SAT instances · Bounded-occurrence 3-SAT instances · Well-formed bounded-occurrence 3-SAT instances · The chain of clauses replacing one clause · Completeness of the chain of one clause · Soundness of the chain of one clause · The tail of a clause chain · Completeness of the tail of a chain · Soundness of the tail of a chain · The 3SAT emitter processes one clause · The SAT-to-3SAT translation preserves satisfiability · The SAT-to-3SAT emitter · Emitter · CNF encodings are nonempty · The 3SAT emitter processes a whole formula · Values of the fresh variables in the 3SAT translation · The SAT-to-3SAT reduction is polynomial-time · Three-literal clause test · The SAT-to-3SAT translation yields clauses of length at most three · Chain clauses have at most three literals · Chain-tail clauses have at most three literals · Clauses of the auxiliary 3SAT translation have at most three literals · Lifting an assignment to the 3SAT translation · The lifted assignment on fresh variables · The lifted assignment on renamed variables · The literals of a clause in the emitter · Output of an emitter on a bit string · The SAT-to-3SAT reduction on bit strings · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Correctness of the clause-length filter · Tokenize, then emit · Correctness of the SAT-to-3SAT reduction on bit strings · The 3SAT decision problem · The SAT-to-3SAT translation · Clause-by-clause translation with a fresh-number counter · Completeness of the auxiliary 3SAT translation · Soundness of the auxiliary 3SAT translation · Output clauses of a walked list of literals · Walking a whole clause gives its chain · MAXIMUM 2-SATISFIABILITY as a decision problem · Feasible MAX-2SAT instances · MAX-2SAT instances · Well-formed MAX-2SAT instances · MAXIMUM SATISFIABILITY as a decision problem · Feasible MAX-SAT instances · MAX-SAT instances · Well-formed MAX-SAT instances · The MINIMUM 2-SATISFIABILITY decision problem · Feasible MINIMUM 2-SATISFIABILITY instances · MINIMUM 2-SATISFIABILITY instances · Well-formed MINIMUM 2-SATISFIABILITY instances · The MINIMUM ONES 3-SAT decision problem · Feasible MINIMUM ONES 3-SAT instances · MINIMUM ONES 3-SAT instances · Well-formed MINIMUM ONES 3-SAT instances · MONOTONE 3-SAT as a decision problem · Satisfiable monotone 3-SAT instances · Monotone 3-SAT instances · Well-formed monotone 3-SAT instances · NOT-ALL-EQUAL 3-SAT as a decision problem · Not-all-equal satisfiability of an instance · NOT-ALL-EQUAL 3-SAT instances · Well-formed NOT-ALL-EQUAL 3-SAT instances · Value of a MAX-3SAT assignment · The MAX-3SAT objective · 2-SAT as a decision problem · SAT with a unary variable count as a decision problem · UniqueSAT with a unary variable count as a decision problem

DefinitionSatisfiability of a CNF formula#✓fully proved

A CNF formula \(\varphi\) is satisfiable when there is an assignment \(v : \mathbb{N} \to \{\mathrm{true}, \mathrm{false}\}\) such that every clause \(C\) of \(\varphi\) contains a literal \((x, b)\) with \(v(x) = b\).

def CNFSat (φ : CNF) : Prop :=
  ∃ v : Nat → Bool, ∀ C ∈ φ, ∃ (x : Nat) (b : Bool), (x, b) ∈ C ∧ v x = b

Uses 2 · Used by 41

Statement usesCNF formula · CNF clause

DefinitionSatisfaction of a literal#✓fully proved

An assignment \(v : \mathbb{N} \to \{\mathrm{true}, \mathrm{false}\}\) satisfies a literal \((x, b)\), with variable \(x \in \mathbb{N}\) and polarity \(b \in \{\mathrm{true}, \mathrm{false}\}\), when \(v(x) = b\).

def Satisfies (assignment : Nat → Bool) (literal : Nat × Bool) : Prop :=
  assignment literal.1 = literal.2

Used by 31

Used bySatisfying a clause through a restricted assignment · Random 3-SAT satisfiability agrees with CNF satisfiability · 2-SAT characterization · Satisfying assignments respect implication edges · Satisfiability means having a satisfying assignment · Satisfaction of a clause · Satisfaction depends only on the occurring variables · Satisfaction of a restricted clause · Satisfaction of a restricted CNF formula · Equivalent CNF · Completeness of a Davis-Putnam step · On Horn formulas, the least model candidate lies below every model · Horn satisfiability via the least model · Counting satisfying assignments over a larger variable range · Unique satisfying extension in the parsimonious 3-CNF reduction · Model count of a CNF formula · Variable compaction preserves the model count · The parsimonious 3-CNF reduction preserves the model count · Satisfaction is preserved by variable compaction · Soundness of the parsimonious 3-CNF reduction · Resolution rule soundness · Tseitin correctness · Satisfaction depends only on the occurring variables · Correctness invariant of the Tseitin encoding · Fixed-length bit-blasting is equisatisfiable · The SAT verifier verifies SAT · Feasible 1-in-3-SAT instances · Completeness of the chain of one clause · Soundness of the chain of one clause · Soundness of the tail of a chain · Not-all-equal satisfiability of an instance

DefinitionSatisfaction of a clause#✓fully proved

An assignment \(v : \mathbb{N} \to \{\mathrm{true}, \mathrm{false}\}\) satisfies a CNF clause \(C\) when at least one literal of \(C\) is satisfied by \(v\), that is, \(C\) contains a literal \((x, b)\) with \(v(x) = b\).

def Satisfies (assignment : Nat → Bool) (clause : CNFClause) : Prop :=
  ∃ literal ∈ clause, CNFLiteral.Satisfies assignment literal

abbrev CNFClause := List (Nat × Bool)

CSLibExt/Logics/Propositional/CNF/Basic.lean:30

def Satisfies (assignment : Nat → Bool) (literal : Nat × Bool) : Prop :=
  assignment literal.1 = literal.2

CSLibExt/Logics/Propositional/CNF/Semantics.lean:32

Uses 2 · Used by 49

Statement usesCNF clause · Satisfaction of a literal

Used bySatisfying a clause through a restricted assignment · Random 3-SAT satisfiability agrees with CNF satisfiability · 2-SAT characterization · Satisfying assignments respect implication edges · Satisfiability means having a satisfying assignment · Satisfiability of a CNF with falsum false · Unit propagation preserves satisfiability · Satisfaction of a CNF formula · Satisfaction depends only on the occurring variables · Satisfaction of a restricted clause · Satisfaction of a restricted CNF formula · Equivalent CNF · Correctness of the Davis-Putnam procedure · Completeness of a Davis-Putnam step · Soundness of a Davis-Putnam step · Correctness of DPLL with sufficient fuel · Correctness of the Horn satisfiability test · On Horn formulas, the least model candidate lies below every model · Horn satisfiability via the least model · Counting satisfying assignments over a larger variable range · Unique satisfying extension in the parsimonious 3-CNF reduction · Model count of a CNF formula · Variable compaction preserves the model count · The parsimonious 3-CNF reduction preserves the model count · Satisfaction is preserved by variable compaction · Soundness of the parsimonious 3-CNF reduction · Refutable formulas are unsatisfiable · Soundness of resolution · Resolution rule soundness · Equisatisfiability of the Tseitin transformation · Tseitin correctness · Satisfying a concatenation of CNF formulas · Satisfaction depends only on the occurring variables · Correctness invariant of the Tseitin encoding · Fixed-length bit-blasting is equisatisfiable · Correctness of the witness clause check · Correctness of the witness formula check · The SAT verifier verifies SAT · The clause check on the occurrence table is the formula check · Completeness of the chain of one clause · Soundness of the chain of one clause · Completeness of the tail of a chain · Soundness of the tail of a chain · Completeness of the auxiliary 3SAT translation · Soundness of the auxiliary 3SAT translation · Feasible MAX-2SAT instances · Feasible MAX-SAT instances · Feasible MINIMUM 2-SATISFIABILITY instances · Not-all-equal satisfiability of an instance

DefinitionSatisfaction of a CNF formula#✓fully proved

An assignment \(v : \mathbb{N} \to \{\mathrm{true}, \mathrm{false}\}\) satisfies a CNF formula \(\varphi\) when \(v\) satisfies every clause of \(\varphi\).

def Satisfies (assignment : Nat → Bool) (formula : CNF) : Prop :=
  ∀ clause ∈ formula, CNFClause.Satisfies assignment clause

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def Satisfies (assignment : Nat → Bool) (clause : CNFClause) : Prop :=
  ∃ literal ∈ clause, CNFLiteral.Satisfies assignment literal

CSLibExt/Logics/Propositional/CNF/Semantics.lean:45

Uses 3 · Used by 56

Statement usesCNF formula · CNF clause · Satisfaction of a clause

Used byRandom 3-SAT satisfiability agrees with CNF satisfiability · 2-SAT characterization · Satisfying assignments respect implication edges · Satisfiability means having a satisfying assignment · Satisfiability of a CNF with falsum false · Unit propagation preserves satisfiability · Splitting on a variable · Satisfaction depends only on the occurring variables · Lifting a satisfying assignment from a restriction · Satisfaction of a restricted CNF formula · Equivalent CNF · Davis-Putnam elimination preserves satisfiability · Correctness of the Davis-Putnam procedure · Completeness of a Davis-Putnam step · Soundness of a Davis-Putnam step · Correctness of DPLL with sufficient fuel · Correctness of the Horn satisfiability test · On Horn formulas, the least model candidate lies below every model · Horn satisfiability via the least model · Counting satisfying assignments over a larger variable range · Unique satisfying extension in the parsimonious 3-CNF reduction · Model count of a CNF formula · Variable compaction preserves the model count · The parsimonious 3-CNF reduction preserves the model count · Satisfaction is preserved by variable compaction · Soundness of the parsimonious 3-CNF reduction · Refutable formulas are unsatisfiable · Soundness of resolution · Equisatisfiability of the Tseitin transformation · Tseitin correctness · Satisfying a concatenation of CNF formulas · Satisfaction depends only on the occurring variables · Tseitin encoding invariant · Correctness invariant of the Tseitin encoding · Evaluation of a quantified CNF formula · UNSAT as a decision problem · Preimage of SAT under a polynomial-time map is in NP · Counting satisfying assignments of a CNF formula · The MAJSAT language · Fixed-length bit-blasting is equisatisfiable · Correctness of the witness formula check · The SAT verifier verifies SAT · The clause check on the occurrence table is the formula check · Satisfiable bounded-occurrence 3-SAT instances · Completeness of the chain of one clause · Soundness of the chain of one clause · Completeness of the tail of a chain · Soundness of the tail of a chain · The SAT-to-3SAT translation preserves satisfiability · Completeness of the auxiliary 3SAT translation · Soundness of the auxiliary 3SAT translation · Feasible MINIMUM ONES 3-SAT instances · Satisfiable monotone 3-SAT instances · 2-SAT as a decision problem · SAT with a unary variable count as a decision problem · UniqueSAT with a unary variable count as a decision problem

TheoremSatisfiability means having a satisfying assignment#✓fully proved

A CNF formula \(\varphi\) is satisfiable if and only if there is an assignment \(v : \mathbb{N} \to \{\mathrm{true}, \mathrm{false}\}\) that satisfies \(\varphi\).

theorem cnfSat_iff_exists_satisfies {formula : CNF} :
    CNFSat formula ↔ ∃ assignment, formula.Satisfies assignment

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def CNFSat (φ : CNF) : Prop :=
  ∃ v : Nat → Bool, ∀ C ∈ φ, ∃ (x : Nat) (b : Bool), (x, b) ∈ C ∧ v x = b

CSLibExt/Logics/Propositional/CNF/Basic.lean:36

Uses 6 · Used by 15

Statement usesCNF formula · Satisfaction of a CNF formula · Satisfiability of a CNF formula

Proof usesCNF clause · Satisfaction of a clause · Satisfaction of a literal

Used byRandom 3-SAT satisfiability agrees with CNF satisfiability · 2-SAT characterization · Satisfiability of a CNF with falsum false · Unit propagation preserves satisfiability · Splitting on a variable · Davis-Putnam elimination preserves satisfiability · Correctness of the Davis-Putnam procedure · Correctness of DPLL with sufficient fuel · Horn satisfiability via the least model · Refutable formulas are unsatisfiable · Equisatisfiability of the Tseitin transformation · Preimage of SAT under a polynomial-time map is in NP · Fixed-length bit-blasting is equisatisfiable · The SAT verifier verifies SAT · The SAT-to-3SAT translation preserves satisfiability

DefinitionDisjunction of two CNFs#✓fully proved

For CNFs \(\varphi = C_1 \land \dots \land C_m\) and \(\psi = D_1 \land \dots \land D_n\), their disjunction is the CNF with one clause \(C_i \lor D_j\) (the literals of \(C_i\) followed by those of \(D_j\)) for each pair \((i, j)\), listed with \(i\) as the outer and \(j\) as the inner index. It expresses \((\bigwedge_i C_i) \lor (\bigwedge_j D_j)\) as \(\bigwedge_{i,j} (C_i \lor D_j)\).

def disj (φ ψ : CNF) : CNF := φ.flatMap fun C ↦ ψ.map fun D ↦ C ++ D

Uses 2 · Used by 3

Statement usesCNF formula · CNF clause

Used byAccumulating CNF builder · Disjoining CNF builder · Equivalent CNF

DefinitionAccumulating CNF builder#✓fully proved

Let \(\iota\) number the atoms by natural numbers, read a literal \((n, p)\) as variable \(n\) with polarity \(p\), and write \(1\) and \(0\) for the polarities true and false. For a polarity \(p\), a proposition \(\varphi\) and a CNF \(S\), the CNF \(\mathcal{A}_p(\varphi, S)\) is defined by recursion on \(\varphi\), together with the disjoining builder \(\mathcal{O}_p\). For an atom \(a\), \(\mathcal{A}_p(a, S)\) is the unit clause \([(\iota(a), p)]\) followed by the clauses of \(S\). Conjunction-like nodes thread the accumulator: \(\mathcal{A}_1(A \land B, S) = \mathcal{A}_1(A, \mathcal{A}_1(B, S))\), \(\mathcal{A}_0(A \lor B, S) = \mathcal{A}_0(A, \mathcal{A}_0(B, S))\) and \(\mathcal{A}_0(A \to B, S) = \mathcal{A}_1(A, \mathcal{A}_0(B, S))\). Disjunction-like nodes go through \(\mathcal{O}\): writing \(X \mathbin{+\!\!+} S\) for the clauses of \(X\) followed by those of \(S\) and \([\,]\) for the empty CNF, \(\mathcal{A}_1(A \lor B, S) = \mathcal{O}_1(A, \mathcal{A}_1(B, [\,])) \mathbin{+\!\!+} S\), \(\mathcal{A}_1(A \to B, S) = \mathcal{O}_0(A, \mathcal{A}_1(B, [\,])) \mathbin{+\!\!+} S\) and \(\mathcal{A}_0(A \land B, S) = \mathcal{O}_0(A, \mathcal{A}_0(B, [\,])) \mathbin{+\!\!+} S\).

An assignment \(\sigma\) satisfies \(\mathcal{A}_p(\varphi, S)\) exactly when \(\varphi\) has truth value \(p\) under \(\sigma \circ \iota\) and \(\sigma\) satisfies \(S\).

def cnfAcc (ι : Atom → ℕ) : Bool → Proposition Atom → CNF → CNF
  | pos, atom a, acc => [(ι a, pos)] :: acc
  | true, and A B, acc => cnfAcc ι true A (cnfAcc ι true B acc)
  | false, or A B, acc => cnfAcc ι false A (cnfAcc ι false B acc)
  | false, imp A B, acc => cnfAcc ι true A (cnfAcc ι false B acc)
  | true, or A B, acc => cnfOr ι true A (cnfAcc ι true B []) ++ acc
  | true, imp A B, acc => cnfOr ι false A (cnfAcc ι true B []) ++ acc
  | false, and A B, acc => cnfOr ι false A (cnfAcc ι false B []) ++ acc

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def cnfOr (ι : Atom → ℕ) : Bool → Proposition Atom → CNF → CNF
  | true, or A B, S => cnfOr ι true A (cnfOr ι true B S)
  | true, imp A B, S => cnfOr ι false A (cnfOr ι true B S)
  | false, and A B, S => cnfOr ι false A (cnfOr ι false B S)
  | pos, atom a, S => CNF.disj [[(ι a, pos)]] S
  | true, and A B, S => CNF.disj (cnfAcc ι true A (cnfAcc ι true B [])) S
  | false, or A B, S => CNF.disj (cnfAcc ι false A (cnfAcc ι false B [])) S
  | false, imp A B, S => CNF.disj (cnfAcc ι true A (cnfAcc ι false B [])) S

CSLibExt/Logics/Propositional/CNF/NormalForm.lean:115

Uses 3 · Used by 2

Statement usesCNF formula · Disjunction of two CNFs · CNF clause

Used byCNF of a proposition at a polarity · Equivalent CNF

DefinitionDisjoining CNF builder#✓fully proved

Let \(\iota\) number the atoms by natural numbers, read a literal \((n, p)\) as variable \(n\) with polarity \(p\), and write \(1\) and \(0\) for the polarities true and false. For a polarity \(p\), a proposition \(\varphi\) and a CNF \(S\), the CNF \(\mathcal{O}_p(\varphi, S)\) is defined by recursion on \(\varphi\), together with the accumulating CNF builder \(\mathcal{A}_p\). Write \(X \otimes S\) for the disjunction of two CNFs \(X\) and \(S\) and \([\,]\) for the empty CNF. For an atom \(a\), \(\mathcal{O}_p(a, S) = U \otimes S\), where \(U\) is the CNF whose only clause is the unit clause \([(\iota(a), p)]\). Disjunction-like nodes are consumed from the left: \(\mathcal{O}_1(A \lor B, S) = \mathcal{O}_1(A, \mathcal{O}_1(B, S))\), \(\mathcal{O}_1(A \to B, S) = \mathcal{O}_0(A, \mathcal{O}_1(B, S))\) and \(\mathcal{O}_0(A \land B, S) = \mathcal{O}_0(A, \mathcal{O}_0(B, S))\). Conjunction-like nodes go through \(\mathcal{A}\): \(\mathcal{O}_1(A \land B, S) = \mathcal{A}_1(A, \mathcal{A}_1(B, [\,])) \otimes S\), \(\mathcal{O}_0(A \lor B, S) = \mathcal{A}_0(A, \mathcal{A}_0(B, [\,])) \otimes S\) and \(\mathcal{O}_0(A \to B, S) = \mathcal{A}_1(A, \mathcal{A}_0(B, [\,])) \otimes S\).

An assignment \(\sigma\) satisfies \(\mathcal{O}_p(\varphi, S)\) exactly when \(\varphi\) has truth value \(p\) under \(\sigma \circ \iota\) or \(\sigma\) satisfies \(S\).

def cnfOr (ι : Atom → ℕ) : Bool → Proposition Atom → CNF → CNF
  | true, or A B, S => cnfOr ι true A (cnfOr ι true B S)
  | true, imp A B, S => cnfOr ι false A (cnfOr ι true B S)
  | false, and A B, S => cnfOr ι false A (cnfOr ι false B S)
  | pos, atom a, S => CNF.disj [[(ι a, pos)]] S
  | true, and A B, S => CNF.disj (cnfAcc ι true A (cnfAcc ι true B [])) S
  | false, or A B, S => CNF.disj (cnfAcc ι false A (cnfAcc ι false B [])) S
  | false, imp A B, S => CNF.disj (cnfAcc ι true A (cnfAcc ι false B [])) S

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def disj (φ ψ : CNF) : CNF := φ.flatMap fun C ↦ ψ.map fun D ↦ C ++ D

CSLibExt/Logics/Propositional/CNF/NormalForm.lean:72

def cnfAcc (ι : Atom → ℕ) : Bool → Proposition Atom → CNF → CNF
  | pos, atom a, acc => [(ι a, pos)] :: acc
  | true, and A B, acc => cnfAcc ι true A (cnfAcc ι true B acc)
  | false, or A B, acc => cnfAcc ι false A (cnfAcc ι false B acc)
  | false, imp A B, acc => cnfAcc ι true A (cnfAcc ι false B acc)
  | true, or A B, acc => cnfOr ι true A (cnfAcc ι true B []) ++ acc
  | true, imp A B, acc => cnfOr ι false A (cnfAcc ι true B []) ++ acc
  | false, and A B, acc => cnfOr ι false A (cnfAcc ι false B []) ++ acc

CSLibExt/Logics/Propositional/CNF/NormalForm.lean:103

Uses 3 · Used by 1

Statement usesCNF formula · Disjunction of two CNFs · CNF clause

Used byEquivalent CNF

DefinitionCNF of a proposition at a polarity#✓fully proved

Let \(\iota\) number the atoms by natural numbers. For a polarity \(p\) and a proposition \(\varphi\), the CNF of \(\varphi\) at polarity \(p\) is the result of the accumulating CNF builder at polarity \(p\) on \(\varphi\) with the empty CNF as accumulator; the atom \(a\) becomes the variable \(\iota(a)\).

An assignment \(\sigma\) satisfies it exactly when \(\varphi\) has truth value \(p\) under \(\sigma \circ \iota\), so it is a CNF of \(\varphi\) when \(p\) is true and of the Boolean complement of \(\varphi\) when \(p\) is false. Only the requested polarity is built: a proposition already in conjunctive normal form gets a CNF of linear size at polarity true, although the CNF of its complement can be exponentially larger.

def cnfOf (ι : Atom → ℕ) (pos : Bool) (A : Proposition Atom) : CNF := cnfAcc ι pos A []

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def cnfAcc (ι : Atom → ℕ) : Bool → Proposition Atom → CNF → CNF
  | pos, atom a, acc => [(ι a, pos)] :: acc
  | true, and A B, acc => cnfAcc ι true A (cnfAcc ι true B acc)
  | false, or A B, acc => cnfAcc ι false A (cnfAcc ι false B acc)
  | false, imp A B, acc => cnfAcc ι true A (cnfAcc ι false B acc)
  | true, or A B, acc => cnfOr ι true A (cnfAcc ι true B []) ++ acc
  | true, imp A B, acc => cnfOr ι false A (cnfAcc ι true B []) ++ acc
  | false, and A B, acc => cnfOr ι false A (cnfAcc ι false B []) ++ acc

CSLibExt/Logics/Propositional/CNF/NormalForm.lean:103

Uses 3 · Used by 3

Statement usesCNF formula · CNF clause · Accumulating CNF builder

Used byEquivalent CNF · CNF of a proposition · CNF of the complement of a proposition

DefinitionCNF of a proposition#✓fully proved

Let \(\iota\) number the atoms by natural numbers. The CNF of a proposition \(A\) is its CNF at polarity true, with the atom \(a\) as the variable \(\iota(a)\).

An assignment \(\sigma\) satisfies it exactly when \(A\) is true under \(\sigma \circ \iota\).

def toCNF (ι : Atom → ℕ) (A : Proposition Atom) : CNF := cnfOf ι true A

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def cnfOf (ι : Atom → ℕ) (pos : Bool) (A : Proposition Atom) : CNF := cnfAcc ι pos A []

CSLibExt/Logics/Propositional/CNF/NormalForm.lean:129

Uses 2 · Used by 2

Statement usesCNF formula · CNF of a proposition at a polarity

Used bySatisfiability of a CNF with falsum false · Equivalent CNF

DefinitionCNF of the complement of a proposition#✓fully proved

Let \(\iota\) number the atoms by natural numbers. The complement CNF of a proposition \(A\) is its CNF at polarity false, with the atom \(a\) as the variable \(\iota(a)\).

An assignment \(\sigma\) satisfies it exactly when \(A\) is false under \(\sigma \circ \iota\). This is not the negation \(\lnot A\), which is \(A \to \bot\) with \(\bot\) an atom: that proposition can be true together with \(A\) when the atom \(\bot\) is true.

def toNegCNF (ι : Atom → ℕ) (A : Proposition Atom) : CNF := cnfOf ι false A

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def cnfOf (ι : Atom → ℕ) (pos : Bool) (A : Proposition Atom) : CNF := cnfAcc ι pos A []

CSLibExt/Logics/Propositional/CNF/NormalForm.lean:129

Uses 2

Statement usesCNF formula · CNF of a proposition at a polarity

TheoremEquivalent CNF#✓fully proved

Let \(\iota\) number the atoms by natural numbers. For every proposition \(A\) and every assignment \(\sigma\) of Boolean values to the natural-number variables, the CNF of \(A\) built with atom \(a\) as variable \(\iota(a)\) is satisfied by \(\sigma\) if and only if \(A\) evaluates to true under the valuation \(\sigma \circ \iota\) of the atoms.

theorem satisfies_toCNF_iff (ι : Atom → ℕ) (A : Proposition Atom) (σ : Nat → Bool) :
    (A.toCNF ι).Satisfies σ ↔ A.evalBool (σ ∘ ι) = true

Uses 11 · Used by 1

Statement usesSatisfaction of a CNF formula · Truth-table evaluation · CNF of a proposition

Proof usesCNF formula · Disjunction of two CNFs · CNF clause · Satisfaction of a clause · Satisfaction of a literal · Accumulating CNF builder · CNF of a proposition at a polarity · Disjoining CNF builder

Used bySatisfiability of a CNF with falsum false

TheoremSatisfiability of a CNF with falsum false#✓fully proved

Let the atoms have a distinguished atom \(\bot\) and let \(\iota\) be an injective numbering of the atoms by natural numbers. For every proposition \(A\), the CNF consisting of the unit clause with the single negative literal on variable \(\iota(\bot)\) followed by the clauses of the CNF of \(A\) (atom \(a\) read as variable \(\iota(a)\)) is satisfiable if and only if some valuation \(v\) of the atoms with \(v(\bot)\) false makes \(A\) true.

theorem cnfSat_toCNF_bot_iff [Bot Atom] {ι : Atom → ℕ} (hι : Function.Injective ι)
    (A : Proposition Atom) :
    CNFSat ([(ι ⊥, false)] :: A.toCNF ι) ↔
      ∃ v : Atom → Bool, v ⊥ = false ∧ A.evalBool v = true

Uses 9

Statement usesCNF clause · Satisfiability of a CNF formula · Truth-table evaluation · CNF of a proposition

Proof usesCNF formula · Satisfaction of a CNF formula · Satisfaction of a clause · Equivalent CNF · Satisfiability means having a satisfying assignment

DefinitionVariables of a clause#✓fully proved

The variables of a CNF clause \(C\) form the finite set of natural numbers \(x\) such that \(C\) contains a literal \((x, b)\) for some polarity \(b\).

def vars (clause : CNFClause) : Finset Nat :=
  (clause.map Prod.fst).toFinset

Uses 1 · Used by 20

Statement usesCNF clause

Used byImplication graph as a finite directed graph · Reachability in the finite implication graph · List of the literals of a CNF formula · Implication edges end over variables of the formula · A positive literal reaching its complement lies over a variable of the formula · The restricted variable no longer occurs · Satisfaction depends only on the occurring variables · Variables of a CNF formula · Restriction does not add variables · Correctness of the Davis-Putnam procedure · Correctness of DPLL with sufficient fuel · Forward-chaining closure · On Horn formulas, the least model candidate lies below every model · Horn satisfiability via the least model · Unique satisfying extension in the parsimonious 3-CNF reduction · Variable compaction preserves the model count · The parsimonious 3-CNF reduction preserves the model count · Compaction preserves absence of duplicate clauses · Variables of a compacted formula form an initial range · Unsatisfiable formulas without variables contain the empty clause

DefinitionRestriction of a clause by a literal#✓fully proved

Given a literal \(\ell = (x, b)\), the restriction of a clause by \(\ell\) is the clause obtained by deleting every literal whose variable is \(x\), of either polarity, keeping the other literals in order.

def restrict (literal : Nat × Bool) (clause : CNFClause) : CNFClause :=
  clause.filter fun candidate ↦ candidate.1 != literal.1

Uses 1 · Used by 7

Statement usesCNF clause

Used byThe restricted variable no longer occurs · Restriction of a CNF formula by a literal · Satisfaction of a restricted clause · Satisfaction of a restricted CNF formula · Restriction does not add variables · Lifting lemma · Clauses of a restricted formula

TheoremSatisfaction of a restricted clause#✓fully proved

Let \(C\) be a clause, \(\ell = (x, b)\) a literal that does not occur in \(C\), and \(v\) an assignment of Booleans to variables with \(v(x) = b\). Then \(v\) satisfies the restriction of \(C\) by \(\ell\) if and only if \(v\) satisfies \(C\).

theorem satisfies_restrict_iff {assignment : Nat → Bool} {literal : Nat × Bool}
    {clause : CNFClause} (hassignment : assignment literal.1 = literal.2)
    (hnot_mem : literal ∉ clause) :
    (clause.restrict literal).Satisfies assignment ↔ clause.Satisfies assignment

Uses 4 · Used by 1

Statement usesCNF clause · Satisfaction of a clause · Restriction of a clause by a literal

Proof usesSatisfaction of a literal

Used bySatisfaction of a restricted CNF formula

DefinitionVariables of a CNF formula#✓fully proved

The variables of a CNF formula \(\varphi\) form the union of the sets of variables of its clauses, that is, the finite set of natural numbers \(x\) such that some clause of \(\varphi\) contains a literal \((x, b)\) for some polarity \(b\).

def vars : CNF → Finset Nat
  | [] => ∅
  | clause :: formula => clause.vars ∪ vars formula

Uses 3 · Used by 33

Statement usesCNF formula · CNF clause · Variables of a clause

Used byAdjacency table of the implication graph · SCC-based 2-SAT decision procedure · Correctness of the SCC-based 2-SAT procedure · Implication graph as a finite directed graph · Reachability in the finite implication graph · Literals over the variables of a formula · List of the literals of a CNF formula · Implication edges end over variables of the formula · A positive literal reaching its complement lies over a variable of the formula · Complement of a literal over a formula · Successors in the implication graph · Restriction reduces the number of variables · The restricted variable no longer occurs · Satisfaction depends only on the occurring variables · Lifting a satisfying assignment from a restriction · Restricting by an occurring variable shrinks the variable set · Restriction does not add variables · Correctness of the Davis-Putnam procedure · The DPLL procedure · Correctness of DPLL with sufficient fuel · Correctness of DPLL · Forward-chaining closure · On Horn formulas, the least model candidate lies below every model · Horn satisfiability via the least model · Counting satisfying assignments over a larger variable range · Unique satisfying extension in the parsimonious 3-CNF reduction · Model count of a CNF formula · Variable compaction preserves the model count · The parsimonious 3-CNF reduction preserves the model count · Compaction preserves absence of duplicate clauses · Variables of a compacted formula form an initial range · Unsatisfiable formulas without variables contain the empty clause · Refutation completeness

DefinitionRestriction of a CNF formula by a literal#✓fully proved

Given a literal \(\ell = (x, b)\), the restriction of a CNF formula \(\varphi\) by \(\ell\) is obtained by deleting every clause of \(\varphi\) that contains \(\ell\) and replacing every other clause by its restriction by \(\ell\), the clause obtained by deleting every literal whose variable is \(x\), of either polarity; the remaining clauses keep their order.

The deleted clauses are true under every assignment that gives \(x\) the value \(b\).

def restrict (literal : Nat × Bool) : CNF → CNF
  | [] => []
  | clause :: formula =>
      if literal ∈ clause then
        restrict literal formula
      else
        clause.restrict literal :: restrict literal formula

Uses 3 · Used by 13

Statement usesCNF formula · CNF clause · Restriction of a clause by a literal

Used byRestriction reduces the number of variables · The restricted variable no longer occurs · Unit propagation preserves satisfiability · Splitting on a variable · Lifting a satisfying assignment from a restriction · Satisfaction of a restricted CNF formula · Restricting by an occurring variable shrinks the variable set · Restriction does not add variables · DPLL with a fuel budget · Correctness of DPLL with sufficient fuel · Lifting lemma · Clauses of a restricted formula · Refutation completeness

TheoremRestriction does not add variables#✓fully proved

For every CNF formula \(\varphi\) and every literal \(\ell\), every variable of the restriction of \(\varphi\) by \(\ell\) is a variable of \(\varphi\).

theorem vars_restrict_subset (literal : Nat × Bool) (formula : CNF) :
    (formula.restrict literal).vars ⊆ formula.vars

Uses 6 · Used by 1

Statement usesCNF formula · Restriction of a CNF formula by a literal · Variables of a CNF formula

Proof usesCNF clause · Restriction of a clause by a literal · Variables of a clause

Used byRestricting by an occurring variable shrinks the variable set

TheoremThe restricted variable no longer occurs#✓fully proved

For every CNF formula \(F\) and every literal \(\ell = (x, b)\), the variable \(x\) does not occur in the restriction of \(F\) by \(\ell\).

@[simp]
theorem not_mem_vars_restrict (literal : Nat × Bool) (formula : CNF) :
    literal.1 ∉ (formula.restrict literal).vars

Uses 6 · Used by 2

Statement usesCNF formula · Restriction of a CNF formula by a literal · Variables of a CNF formula

Proof usesCNF clause · Restriction of a clause by a literal · Variables of a clause

Used byLifting a satisfying assignment from a restriction · Restricting by an occurring variable shrinks the variable set

TheoremRestricting by an occurring variable shrinks the variable set#✓fully proved

Let \(\varphi\) be a CNF formula and \((x, b)\) a literal. If \(x\) is a variable of \(\varphi\), then the set of variables of the restriction of \(\varphi\) by \((x, b)\) is a proper subset of the set of variables of \(\varphi\).

theorem vars_restrict_ssubset {literal : Nat × Bool} {formula : CNF}
    (hmem : literal.1 ∈ formula.vars) :
    (formula.restrict literal).vars ⊂ formula.vars

Uses 5 · Used by 1

Statement usesCNF formula · Restriction of a CNF formula by a literal · Variables of a CNF formula

Proof usesThe restricted variable no longer occurs · Restriction does not add variables

Used byRestriction reduces the number of variables

TheoremRestriction reduces the number of variables#✓fully proved

Let \(F\) be a CNF formula and let \(\ell = (x, b)\) be a literal whose variable \(x\) occurs in \(F\). Then the restriction of \(F\) by \(\ell\) has strictly fewer distinct variables than \(F\).

theorem card_vars_restrict_lt {literal : Nat × Bool} {formula : CNF}
    (hmem : literal.1 ∈ formula.vars) :
    (formula.restrict literal).vars.card < formula.vars.card

Uses 4 · Used by 2

Statement usesCNF formula · Restriction of a CNF formula by a literal · Variables of a CNF formula

Proof usesRestricting by an occurring variable shrinks the variable set

Used byCorrectness of DPLL with sufficient fuel · Refutation completeness

TheoremSatisfaction of a restricted CNF formula#✓fully proved

Let \(\varphi\) be a CNF formula, \(\ell = (x, b)\) a literal, and \(v\) an assignment of Booleans to variables with \(v(x) = b\). Then \(v\) satisfies the restriction of \(\varphi\) by \(\ell\) if and only if \(v\) satisfies \(\varphi\).

theorem satisfies_restrict_iff {assignment : Nat → Bool} {literal : Nat × Bool}
    {formula : CNF} (hassignment : assignment literal.1 = literal.2) :
    (formula.restrict literal).Satisfies assignment ↔ formula.Satisfies assignment

Uses 8 · Used by 3

Statement usesCNF formula · Satisfaction of a CNF formula · Restriction of a CNF formula by a literal

Proof usesCNF clause · Satisfaction of a clause · Restriction of a clause by a literal · Satisfaction of a restricted clause · Satisfaction of a literal

Used byUnit propagation preserves satisfiability · Splitting on a variable · Lifting a satisfying assignment from a restriction

TheoremSatisfaction depends only on the occurring variables#✓fully proved

Let \(F\) be a CNF formula and let \(v_1, v_2\) be assignments of Booleans to variables with \(v_1(x) = v_2(x)\) for every variable \(x\) occurring in \(F\). If \(v_1\) satisfies \(F\), then \(v_2\) satisfies \(F\).

theorem satisfies_congr {formula : CNF} {assignment₁ assignment₂ : Nat → Bool}
    (hagrees : ∀ x ∈ formula.vars, assignment₁ x = assignment₂ x)
    (hsatisfies : formula.Satisfies assignment₁) :
    formula.Satisfies assignment₂

Uses 7 · Used by 3

Statement usesCNF formula · Satisfaction of a CNF formula · Variables of a CNF formula

Proof usesCNF clause · Satisfaction of a clause · Variables of a clause · Satisfaction of a literal

Used byLifting a satisfying assignment from a restriction · Counting satisfying assignments over a larger variable range · The parsimonious 3-CNF reduction preserves the model count

TheoremLifting a satisfying assignment from a restriction#✓fully proved

Let \(F\) be a CNF formula, \(\ell = (x, b)\) a literal and \(v\) an assignment of Booleans to variables. If \(v\) satisfies the restriction of \(F\) by \(\ell\), then the assignment that agrees with \(v\) except that it sends \(x\) to \(b\) satisfies \(F\).

theorem satisfies_of_satisfies_restrict {formula : CNF} {assignment : Nat → Bool}
    {literal : Nat × Bool} (hsatisfies : (formula.restrict literal).Satisfies assignment) :
    formula.Satisfies (Function.update assignment literal.1 literal.2)

Uses 7 · Used by 2

Statement usesCNF formula · Satisfaction of a CNF formula · Restriction of a CNF formula by a literal

Proof usesThe restricted variable no longer occurs · Satisfaction depends only on the occurring variables · Satisfaction of a restricted CNF formula · Variables of a CNF formula

Used byUnit propagation preserves satisfiability · Splitting on a variable

TheoremSplitting on a variable#✓fully proved

For every CNF formula \(F\) and every variable \(x\), the formula \(F\) is satisfiable if and only if the restriction of \(F\) by the literal \((x, \mathrm{true})\) is satisfiable or the restriction of \(F\) by the literal \((x, \mathrm{false})\) is satisfiable.

theorem sat_iff_restrict_true_or_false (formula : CNF) (x : Nat) :
    CNFSat formula ↔
      CNFSat (formula.restrict (x, true)) ∨ CNFSat (formula.restrict (x, false))

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def CNFSat (φ : CNF) : Prop :=
  ∃ v : Nat → Bool, ∀ C ∈ φ, ∃ (x : Nat) (b : Bool), (x, b) ∈ C ∧ v x = b

CSLibExt/Logics/Propositional/CNF/Basic.lean:36

Uses 7 · Used by 2

Statement usesCNF formula · Restriction of a CNF formula by a literal · Satisfiability of a CNF formula

Proof usesSatisfaction of a CNF formula · Lifting a satisfying assignment from a restriction · Satisfaction of a restricted CNF formula · Satisfiability means having a satisfying assignment

Used byCorrectness of DPLL with sufficient fuel · Refutation completeness

TheoremUnit propagation preserves satisfiability#✓fully proved

Let \(F\) be a CNF formula that contains the unit clause whose only literal is \(\ell\). Then \(F\) is satisfiable if and only if the restriction of \(F\) by \(\ell\) is satisfiable.

theorem sat_iff_restrict_of_unit {formula : CNF} {literal : Nat × Bool}
    (hunit : [literal] ∈ formula) :
    CNFSat formula ↔ CNFSat (formula.restrict literal)

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def CNFSat (φ : CNF) : Prop :=
  ∃ v : Nat → Bool, ∀ C ∈ φ, ∃ (x : Nat) (b : Bool), (x, b) ∈ C ∧ v x = b

CSLibExt/Logics/Propositional/CNF/Basic.lean:36

Uses 9 · Used by 1

Statement usesCNF formula · Restriction of a CNF formula by a literal · CNF clause · Satisfiability of a CNF formula

Proof usesSatisfaction of a CNF formula · Lifting a satisfying assignment from a restriction · Satisfaction of a restricted CNF formula · Satisfaction of a clause · Satisfiability means having a satisfying assignment

Used byCorrectness of DPLL with sufficient fuel

29 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.