Conjunctive normal form

Propositional formulas in conjunctive normal form over an arbitrary type of variables V, with their Boolean semantics. A literal (Std.Sat.Literal) is a variable together with the polarity under which it is read, a clause is a list of literals read disjunctively, and a formula is a list of clauses read conjunctively.

Formulas are plain lists so that reductions can build them with list operations and their sizes can be read off directly. This is why Std.Sat.CNF, an array-based structure built for efficient SAT solving in bv_decide, is not reused; neither is Cslib.Logic.PL.Proposition, whose connectives are binary and whose formulas are not in normal form. The names follow Std.Sat.CNF where they overlap (relabel, eval).

Reductions to satisfiability usually build formulas over structured variables (indexed by time steps, tape cells, and so on) and relabel them injectively at the end; CNF.satisfiable_relabel says that this preserves satisfiability.

Main definitions

• Cslib.Logic.PL.Literal, Clause, CNF.
• Cslib.Logic.PL.CNF.eval, Cslib.Logic.PL.CNF.Satisfiable.
• Cslib.Logic.PL.CNF.vars: the variables of a formula, in order of occurrence.
• Cslib.Logic.PL.CNF.relabel: rename the variables of a formula.
• Cslib.Logic.PL.CNF.countUnsat: the number of clauses an assignment falsifies.
• Cslib.Logic.PL.Clause.imp, Cslib.Logic.PL.Clause.impLits: the clause h₁ ∧ ⋯ ∧ hₙ → c, for variables or literals hᵢ.

Main results

• Cslib.Logic.PL.CNF.eval_eq_true_iff, Cslib.Logic.PL.Clause.eval_eq_true_iff: the semantics as quantifiers over clauses and literals.
• Cslib.Logic.PL.CNF.eval_congr: a formula only depends on its variables.
• Cslib.Logic.PL.CNF.mem_vars, Cslib.Logic.PL.CNF.vars_relabel, Cslib.Logic.PL.Clause.fst_mem_of_mem_imp: the variables of formulas and implications.
• Cslib.Logic.PL.CNF.satisfiable_relabel: injective relabelling preserves satisfiability.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3

@[reducible, inline]

abbrev Cslib.Logic.PL.Literal (V : Type u_1) : Type u_1

A literal: a variable and the polarity under which it is read.

@[reducible, inline]

abbrev Cslib.Logic.PL.Clause (V : Type u_1) : Type u_1

A clause is a disjunction of literals.

@[reducible, inline]

abbrev Cslib.Logic.PL.CNF (V : Type u_1) : Type u_1

A formula in conjunctive normal form is a conjunction of clauses.

def Cslib.Logic.PL.Literal.eval {V : Type u_1} (σ : V → Bool) (l : Literal V) : Bool

A literal (v, b) holds under σ when σ v = b.

def Cslib.Logic.PL.Clause.eval {V : Type u_1} (σ : V → Bool) (c : Clause V) : Bool

A clause holds when one of its literals does.

def Cslib.Logic.PL.CNF.eval {V : Type u_1} (σ : V → Bool) (φ : CNF V) : Bool

A formula holds when all of its clauses do.

def Cslib.Logic.PL.CNF.Satisfiable {V : Type u_1} (φ : CNF V) : Prop

A formula is satisfiable when some assignment makes it true.

Semantics

@[simp]

theorem Cslib.Logic.PL.Literal.eval_mk {V : Type u_1} (σ : V → Bool) (v : V) (b : Bool) : eval σ (v, b) = (σ v == b)

The value of a literal (v, b): whether v has the value b.

@[simp]

theorem Cslib.Logic.PL.Literal.eval_eq_true_iff {V : Type u_1} (σ : V → Bool) (l : Literal V) : eval σ l = true ↔ σ l.fst = l.snd

A literal holds when its variable has its polarity.

@[simp]

theorem Cslib.Logic.PL.Literal.eval_negate {V : Type u_1} (σ : V → Bool) (l : Literal V) : eval σ (Std.Sat.Literal.negate l) = !eval σ l

Negating a literal negates its value.

theorem Cslib.Logic.PL.Clause.eval_eq_true_iff {V : Type u_1} (σ : V → Bool) (c : Clause V) : eval σ c = true ↔ ∃ (l : Literal V), l ∈ c ∧ σ l.fst = l.snd

A clause holds when some literal does.

@[simp]

theorem Cslib.Logic.PL.Clause.eval_nil {V : Type u_1} (σ : V → Bool) : eval σ [] = false

@[simp]

theorem Cslib.Logic.PL.Clause.eval_cons {V : Type u_1} (σ : V → Bool) (l : Literal V) (c : Clause V) : eval σ (l :: c) = (Literal.eval σ l || eval σ c)

theorem Cslib.Logic.PL.CNF.eval_eq_true_iff {V : Type u_1} (σ : V → Bool) (φ : CNF V) : eval σ φ = true ↔ ∀ (c : Clause V), c ∈ φ → Clause.eval σ c = true

A formula holds when every clause does.

@[simp]

theorem Cslib.Logic.PL.CNF.eval_nil {V : Type u_1} (σ : V → Bool) : eval σ [] = true

@[simp]

theorem Cslib.Logic.PL.CNF.eval_append {V : Type u_1} (σ : V → Bool) (φ ψ : CNF V) : eval σ (φ ++ ψ) = (eval σ φ && eval σ ψ)

@[simp]

theorem Cslib.Logic.PL.CNF.eval_cons {V : Type u_1} (σ : V → Bool) (c : Clause V) (φ : CNF V) : eval σ (c :: φ) = (Clause.eval σ c && eval σ φ)

theorem Cslib.Logic.PL.CNF.eval_map_eq_true_iff {V : Type u_1} {ι : Type u_3} (σ : V → Bool) (l : List ι) (f : ι → Clause V) : eval σ (List.map f l) = true ↔ ∀ (i : ι), i ∈ l → Clause.eval σ (f i) = true

A formula made of one clause per element of a list holds when each of those clauses does.

theorem Cslib.Logic.PL.CNF.eval_flatMap_eq_true_iff {V : Type u_1} {ι : Type u_3} (σ : V → Bool) (l : List ι) (f : ι → CNF V) : eval σ (List.flatMap f l) = true ↔ ∀ (i : ι), i ∈ l → eval σ (f i) = true

A formula made of one block of clauses per element of a list holds when each block does.

Variables

def Cslib.Logic.PL.CNF.vars {V : Type u_1} (φ : CNF V) : List V

The variables of a formula, in order of occurrence and with repetitions.

theorem Cslib.Logic.PL.CNF.length_vars {V : Type u_1} (φ : CNF V) : φ.vars.length = (List.map List.length φ).sum

theorem Cslib.Logic.PL.CNF.length_vars_le_mul_length {V : Type u_1} {k : ℕ} {φ : CNF V} (h : ∀ (c : Clause V), c ∈ φ → List.length c ≤ k) : φ.vars.length ≤ k * List.length φ

A formula with m clauses of at most k literals has at most k m occurrences of variables.

theorem Cslib.Logic.PL.CNF.mem_vars {V : Type u_1} {φ : CNF V} {v : V} : v ∈ φ.vars ↔ ∃ (c : Clause V), c ∈ φ ∧ ∃ (b : Bool), (v, b) ∈ c

A variable of a formula is the variable of a literal of one of its clauses.

theorem Cslib.Logic.PL.CNF.eval_congr {V : Type u_1} {σ τ : V → Bool} {φ : CNF V} (h : ∀ (v : V), v ∈ φ.vars → σ v = τ v) : eval σ φ = eval τ φ

A formula only depends on the values of its variables.

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

The number of clauses of a formula, counted with repetition, mentioning the variable v.

Implications

def Cslib.Logic.PL.Clause.impLits {V : Type u_1} (hyps : List (Literal V)) (concl : V) : Clause V

The clause l₁ ∧ ⋯ ∧ lₙ → c for literals lᵢ, that is ¬l₁ ∨ ⋯ ∨ ¬lₙ ∨ c.

@[simp]

theorem Cslib.Logic.PL.Clause.eval_impLits {V : Type u_1} (σ : V → Bool) (hyps : List (Literal V)) (concl : V) : eval σ (impLits hyps concl) = true ↔ (∀ (l : Literal V), l ∈ hyps → σ l.fst = l.snd) → σ concl = true

def Cslib.Logic.PL.Clause.imp {V : Type u_1} (hyps : List V) (concl : V) : Clause V

The clause h₁ ∧ ⋯ ∧ hₙ → c, that is ¬h₁ ∨ ⋯ ∨ ¬hₙ ∨ c.

@[simp]

theorem Cslib.Logic.PL.Clause.eval_imp {V : Type u_1} (σ : V → Bool) (hyps : List V) (concl : V) : eval σ (imp hyps concl) = true ↔ (∀ (h : V), h ∈ hyps → σ h = true) → σ concl = true

theorem Cslib.Logic.PL.Clause.fst_mem_of_mem_impLits {V : Type u_1} {hyps : List (Literal V)} {concl : V} {l : Literal V} (hl : l ∈ impLits hyps concl) : (∃ (h : Literal V), h ∈ hyps ∧ l.fst = h.fst) ∨ l.fst = concl

The variables of an implication are its hypotheses and its conclusion.

theorem Cslib.Logic.PL.Clause.fst_mem_of_mem_imp {V : Type u_1} {hyps : List V} {concl : V} {l : Literal V} (hl : l ∈ imp hyps concl) : l.fst ∈ hyps ∨ l.fst = concl

The variables of an implication are its hypotheses and its conclusion.

Relabelling

def Cslib.Logic.PL.Clause.relabel {V : Type u_1} {W : Type u_2} (f : V → W) (c : Clause V) : Clause W

Rename the variables of a clause along f.

def Cslib.Logic.PL.CNF.relabel {V : Type u_1} {W : Type u_2} (f : V → W) (φ : CNF V) : CNF W

Rename the variables of a formula along f.

@[simp]

theorem Cslib.Logic.PL.Clause.relabel_id {V : Type u_1} (c : Clause V) : relabel id c = c

@[simp]

theorem Cslib.Logic.PL.CNF.relabel_id {V : Type u_1} (φ : CNF V) : relabel id φ = φ

@[simp]

theorem Cslib.Logic.PL.Clause.eval_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (σ : W → Bool) (c : Clause V) : eval σ (relabel f c) = eval (σ ∘ f) c

@[simp]

theorem Cslib.Logic.PL.CNF.eval_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (σ : W → Bool) (φ : CNF V) : eval σ (relabel f φ) = eval (σ ∘ f) φ

@[simp]

theorem Cslib.Logic.PL.Clause.length_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (c : Clause V) : List.length (relabel f c) = List.length c

theorem Cslib.Logic.PL.CNF.vars_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (φ : CNF V) : (relabel f φ).vars = List.map f φ.vars

Relabelling renames the variables, occurrence by occurrence.

theorem Cslib.Logic.PL.CNF.satisfiable_relabel {V : Type u_1} {W : Type u_2} {f : V → W} (hf : Function.Injective f) (φ : CNF V) : (relabel f φ).Satisfiable ↔ φ.Satisfiable

Relabelling along an injective map preserves satisfiability. An assignment of the new variables restricts to the old ones, and an assignment of the old variables extends along f.

def Cslib.Logic.PL.CNF.countUnsat {V : Type u_1} (σ : V → Bool) (φ : CNF V) : ℕ

The number of clauses of φ, counted with multiplicity, that the assignment σ falsifies.

theorem Cslib.Logic.PL.CNF.countUnsat_eq_zero_iff {V : Type u_1} {σ : V → Bool} {φ : CNF V} : countUnsat σ φ = 0 ↔ eval σ φ = true

An assignment falsifies no clause exactly when it satisfies the formula.

theorem Cslib.Logic.PL.CNF.countUnsat_le_length {V : Type u_1} (σ : V → Bool) (φ : CNF V) : countUnsat σ φ ≤ List.length φ

An assignment falsifies at most all the clauses.