Clause sets

A clause set is a finite set of clauses, each a finite set of literals: the set-based form of a formula in conjunctive normal form, in which the order and repetition of clauses and literals do not matter. Set operations on clauses (subclauses, differences) are what the sparsification lemma works with. A formula in conjunctive normal form and its clause set have the same solutions (CNF.sat_toClauseSet_iff), and a clause set is the clause set of a formula listing its clauses (ClauseSet.eval_toCNF_eq_true_iff).

Main definitions

• Cslib.Logic.PL.ClauseSet: finite sets of finite sets of literals.
• Cslib.Logic.PL.ClauseSet.Sat, Cslib.Logic.PL.ClauseSet.solutions: satisfaction.
• Cslib.Logic.PL.ClauseSet.occurrences: the number of clauses mentioning a variable.
• Cslib.Logic.PL.CNF.toClauseSet, Cslib.Logic.PL.ClauseSet.toCNF: the translations.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3
• C. Calabro, R. Impagliazzo, R. Paturi, A duality between clause width and clause density for SAT

theorem Cslib.Logic.PL.card_literal {V : Type u_1} [Fintype V] : Fintype.card (Literal V) = 2 * Fintype.card V

There are two literals for each variable.

@[reducible, inline]

abbrev Cslib.Logic.PL.ClauseSet (V : Type u_2) : Type u_2

A clause set: a finite set of clauses, each a finite set of literals. A clause is satisfied when one of its literals is true; a clause set when all of its clauses are.

def Cslib.Logic.PL.ClauseSet.Sat {V : Type u_1} (ψ : ClauseSet V) (x : V → Bool) : Prop

x satisfies every clause of ψ.

@[instance_reducible]

instance Cslib.Logic.PL.ClauseSet.instDecidableSat {V : Type u_1} (ψ : ClauseSet V) (x : V → Bool) : Decidable (ψ.Sat x)

def Cslib.Logic.PL.ClauseSet.solutions {V : Type u_1} [DecidableEq V] [Fintype V] (ψ : ClauseSet V) : Finset (V → Bool)

The solutions of a clause set.

@[simp]

theorem Cslib.Logic.PL.ClauseSet.mem_solutions {V : Type u_1} [DecidableEq V] [Fintype V] {ψ : ClauseSet V} {x : V → Bool} : x ∈ ψ.solutions ↔ ψ.Sat x

def Cslib.Logic.PL.ClauseSet.occurrences {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (v : V) : ℕ

The number of clauses of ψ mentioning the variable v.

def Cslib.Logic.PL.CNF.toClauseSet {V : Type u_1} [DecidableEq V] (φ : CNF V) : ClauseSet V

The clause set of a formula in conjunctive normal form.

theorem Cslib.Logic.PL.CNF.sat_toClauseSet_iff {V : Type u_1} [DecidableEq V] (φ : CNF V) (x : V → Bool) : φ.toClauseSet.Sat x ↔ eval x φ = true

A formula in conjunctive normal form and its clause set have the same solutions.

theorem Cslib.Logic.PL.CNF.exists_card_le_of_mem_toClauseSet {V : Type u_1} [DecidableEq V] {φ : CNF V} {C : Finset (Literal V)} (hC : C ∈ φ.toClauseSet) : ∃ c ∈ φ, C.card ≤ List.length c

A clause of the clause set of a formula has at most as many literals as the clause it comes from.

noncomputable def Cslib.Logic.PL.ClauseSet.toCNF {V : Type u_1} (ψ : ClauseSet V) : CNF V

A formula listing the clauses of a clause set.

theorem Cslib.Logic.PL.ClauseSet.eval_toCNF_eq_true_iff {V : Type u_1} (ψ : ClauseSet V) (x : V → Bool) : CNF.eval x ψ.toCNF = true ↔ ψ.Sat x

The formula of a clause set accepts exactly its solutions.

theorem Cslib.Logic.PL.ClauseSet.length_le_of_mem_toCNF {V : Type u_1} {ψ : ClauseSet V} {k : ℕ} (hk : ∀ C ∈ ψ, C.card ≤ k) {c : Clause V} (hc : c ∈ ψ.toCNF) : List.length c ≤ k

The clauses of the formula of a clause set have at most as many literals as its clauses.

theorem Cslib.Logic.PL.ClauseSet.occurrences_toCNF {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (v : V) : ψ.toCNF.occurrences v = ψ.occurrences v

The formula of a clause set has as many clauses mentioning v as the clause set.