Satisfiability of CNF structures

A formula in conjunctive normal form is given as a finite structure for the vocabulary cnf of two binary relation symbols cnf.pos and cnf.neg. Every element c names a clause and a variable: the clause named by c has the positive literal x when pos(c, x) holds and the negative literal ¬x when neg(c, x) holds. An element related to nothing names the empty clause. A structure is satisfiable (cnf.Satisfiable) when some assignment of truth values to the elements satisfies every clause, that is, when it satisfies the existential second-order sentence ∃ S, ∀ c, ∃ x, (pos(c, x) ∧ S x) ∨ (neg(c, x) ∧ ¬ S x). It is a 3-CNF structure (cnf.IsThreeCNF) when every clause has at most three literals.

Descriptive complexity presents satisfiability as a class of finite structures in this way Immerman, Chapter 7; the conventions above are fixed here. A formula with m clauses over n variables is presented by a structure with max m n elements: the clauses and the variables are numbered from the same elements, and the elements naming no clause of the formula name the tautology x ∨ ¬x of their own variable. The empty structure presents the empty formula, which is satisfiable. The machine-level problem, on formulas of Cslib.Logic.PL.CNF ℕ encoded as lists, is Cslib.Complexity.SAT.

The classes cnf.SAT and cnf.ThreeSAT of satisfiable structures and of satisfiable 3-CNF structures are existential second-order definable, hence closed under isomorphism, and they are invariant under disjoint copies, so that tagged interpretations reduce to them. The vocabulary cnf.vocabulary lists the table of pos before that of neg in encoded structures.

Main definitions

• Cslib.Logic.FO.cnf: the vocabulary of CNF structures, with cnf.pos and cnf.neg.
• Cslib.Logic.FO.cnf.literals: the literals of the clause named by an element.
• Cslib.Logic.FO.cnf.ClauseSatisfied, Cslib.Logic.FO.cnf.Satisfies, Cslib.Logic.FO.cnf.Satisfiable: satisfied clauses, satisfying assignments and satisfiability.
• Cslib.Logic.FO.cnf.IsThreeCNF: every clause has at most three literals.
• Cslib.Logic.FO.cnf.SAT, Cslib.Logic.FO.cnf.ThreeSAT: the classes SAT and 3SAT.
• Cslib.Logic.FO.cnf.satSentence, Cslib.Logic.FO.cnf.threeCNFSentence: their defining existential second-order and first-order sentences.
• Cslib.Logic.FO.cnf.vocabulary: the vocabulary of encoded CNF structures.

Main results

• Cslib.Logic.FO.cnf.realize_satSentence, Cslib.Logic.FO.cnf.realize_threeCNFSentence: the semantics of the defining sentences.
• Cslib.Logic.FO.cnf.definable_SAT, Cslib.Logic.FO.cnf.definable_ThreeSAT: SAT and 3SAT are existential second-order definable.
• Cslib.Logic.FO.cnf.isoClosed_SAT, Cslib.Logic.FO.cnf.copyInvariant_SAT and their 3SAT versions.
• Cslib.Logic.FO.cnf.clauseSatisfied_iff_of_templates: the clauses of a CNF structure interpreted by templates.

References

• N. Immerman, Descriptive Complexity

The vocabulary

inductive Cslib.Logic.FO.CNFRel : ℕ → Type

The relation symbols of CNF structures.

• pos : CNFRel 2

  The positive occurrence of a variable in a clause.

• neg : CNFRel 2

  The negative occurrence of a variable in a clause.

@[instance_reducible]

instance Cslib.Logic.FO.instDecidableEqCNFRel {a✝ : ℕ} : DecidableEq (CNFRel a✝)

def Cslib.Logic.FO.instDecidableEqCNFRel.decEq {a✝ : ℕ} (x✝ x✝¹ : CNFRel a✝) : Decidable (x✝ = x✝¹)

def Cslib.Logic.FO.cnf : FirstOrder.Language

The vocabulary of CNF structures, with two binary relation symbols.

instance Cslib.Logic.FO.instIsRelationalCnf : cnf.IsRelational

@[reducible, inline]

abbrev Cslib.Logic.FO.cnf.pos : cnf.Relations 2

pos(c, x): the variable x occurs positively in the clause c.

@[reducible, inline]

abbrev Cslib.Logic.FO.cnf.neg : cnf.Relations 2

neg(c, x): the variable x occurs negatively in the clause c.

def Cslib.Logic.FO.cnf.lit : Bool → cnf.Relations 2

The relation symbol of the literals of a polarity: pos for true, neg for false.

@[simp]

theorem Cslib.Logic.FO.cnf.lit_true : lit true = cnf.pos

@[simp]

theorem Cslib.Logic.FO.cnf.lit_false : lit false = cnf.neg

Satisfiability

def Cslib.Logic.FO.cnf.literals {M : Type u_1} [cnf.Structure M] (c : M) : Set (Bool × M)

The literals of the clause named by c: a polarity and a variable.

theorem Cslib.Logic.FO.cnf.mem_literals {M : Type u_1} [cnf.Structure M] {c : M} {l : Bool × M} : l ∈ literals c ↔ FirstOrder.Language.Structure.RelMap (lit l.1) ![c, l.2]

def Cslib.Logic.FO.cnf.ClauseSatisfied {M : Type u_1} [cnf.Structure M] (A : M → Prop) (c : M) : Prop

An assignment satisfies the clause named by c when the clause has a positive literal whose variable is true or a negative literal whose variable is false.

def Cslib.Logic.FO.cnf.Satisfies {M : Type u_1} [cnf.Structure M] (A : M → Prop) : Prop

An assignment satisfies a CNF structure when it satisfies every clause.

def Cslib.Logic.FO.cnf.Satisfiable (M : Type u_3) [cnf.Structure M] : Prop

A CNF structure is satisfiable when some assignment satisfies it.

theorem Cslib.Logic.FO.cnf.clauseSatisfied_iff {M : Type u_1} [cnf.Structure M] (A : M → Prop) (c : M) : ClauseSatisfied A c ↔ ∃ l ∈ literals c, A l.2 ↔ l.1 = true

A clause is satisfied when it has a literal with the truth value of its polarity.

theorem Cslib.Logic.FO.cnf.satisfies_iff {M : Type u_1} [cnf.Structure M] (A : M → Prop) : Satisfies A ↔ ∀ (c : M), ∃ l ∈ literals c, A l.2 ↔ l.1 = true

theorem Cslib.Logic.FO.cnf.Satisfiable.of_equiv {M : Type u_1} [cnf.Structure M] {N : Type u_2} [cnf.Structure N] (e : cnf.Equiv M N) (h : Satisfiable M) : Satisfiable N

Satisfiability is invariant under isomorphism.

theorem Cslib.Logic.FO.cnf.satisfiable_iff_of_equiv {M : Type u_1} [cnf.Structure M] {N : Type u_2} [cnf.Structure N] (e : cnf.Equiv M N) : Satisfiable M ↔ Satisfiable N

theorem Cslib.Logic.FO.cnf.Satisfiable.literals_nonempty {M : Type u_1} [cnf.Structure M] (h : Satisfiable M) (c : M) : (literals c).Nonempty

Every clause of a satisfiable CNF structure is nonempty.

3-CNF structures

def Cslib.Logic.FO.cnf.IsThreeCNF (M : Type u_3) [cnf.Structure M] : Prop

A CNF structure is a 3-CNF structure when every clause has at most three literals.

theorem Cslib.Logic.FO.cnf.encard_literals_le_three_iff {M : Type u_1} [cnf.Structure M] (c : M) : (literals c).encard ≤ 3 ↔ ¬∃ (l : Fin 4 → Bool × M), (∀ (i : Fin 4), l i ∈ literals c) ∧ Function.Injective l

A clause has at most three literals exactly when it has no four distinct ones.

theorem Cslib.Logic.FO.cnf.isThreeCNF_iff_of_equiv {M : Type u_1} [cnf.Structure M] {N : Type u_2} [cnf.Structure N] (e : cnf.Equiv M N) : IsThreeCNF M ↔ IsThreeCNF N

The classes SAT and 3SAT

def Cslib.Logic.FO.cnf.SAT : Set (CategoryTheory.Bundled cnf.Structure)

SAT: the class of satisfiable CNF structures.

def Cslib.Logic.FO.cnf.ThreeSAT : Set (CategoryTheory.Bundled cnf.Structure)

3SAT: the class of satisfiable 3-CNF structures.

theorem Cslib.Logic.FO.cnf.isoClosed_SAT : IsoClosed SAT

SAT is closed under isomorphism.

theorem Cslib.Logic.FO.cnf.isoClosed_ThreeSAT : IsoClosed ThreeSAT

3SAT is closed under isomorphism.

theorem Cslib.Logic.FO.cnf.satisfiable_of_isEmpty {M : Type u_1} [cnf.Structure M] [IsEmpty M] : Satisfiable M

The empty structure is satisfiable.

theorem Cslib.Logic.FO.cnf.isThreeCNF_of_isEmpty {M : Type u_1} [cnf.Structure M] [IsEmpty M] : IsThreeCNF M

The empty structure is a 3-CNF structure.

theorem Cslib.Logic.FO.cnf.isThreeCNF_of_subsingleton {M : Type u_1} [cnf.Structure M] [Subsingleton M] : IsThreeCNF M

Every structure with at most one element is a 3-CNF structure.

Copies

theorem Cslib.Logic.FO.cnf.copyInvariant_SAT : CopyInvariant SAT

SAT is invariant under copies.

theorem Cslib.Logic.FO.cnf.copyInvariant_ThreeSAT : CopyInvariant ThreeSAT

3SAT is invariant under copies.

CNF structures interpreted by templates

theorem Cslib.Logic.FO.cnf.relMap_lit_of_templates {L : FirstOrder.Language} {T : Type u_3} {ι : T → Type u_4} [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L cnf T ι} {temps : (t : T) → Bool → List (TaggedInterpretation.Template L ι t)} {M : Type w} [L.Structure M] (hI : ∀ (b : Bool) (ts : Fin 2 → T), I.rel (lit b) ts = TaggedInterpretation.binaryRel (fun (t w : T) => TaggedInterpretation.Template.listFormula (temps t b) w) ts) (b : Bool) (c y : I.Model M) : FirstOrder.Language.Structure.RelMap (lit b) ![c, y] ↔ ∃ τ ∈ temps c.fst b, τ.Holds (↑c.snd) y.toSigma

In a CNF structure interpreted by templates, the literals of a polarity of a clause are the elements related to it by the templates of that polarity.

theorem Cslib.Logic.FO.cnf.clauseSatisfied_iff_of_templates {L : FirstOrder.Language} {T : Type u_3} {ι : T → Type u_4} [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L cnf T ι} {temps : (t : T) → Bool → List (TaggedInterpretation.Template L ι t)} {M : Type w} [L.Structure M] (hI : ∀ (b : Bool) (ts : Fin 2 → T), I.rel (lit b) ts = TaggedInterpretation.binaryRel (fun (t w : T) => TaggedInterpretation.Template.listFormula (temps t b) w) ts) (A : I.Model M → Prop) (c : I.Model M) : ClauseSatisfied A c ↔ (∃ τ ∈ temps c.fst true, τ.guard.Realize ↑c.snd ∧ ∃ (y : ι τ.target → M) (hy : (I.domain τ.target).Realize y), τ.Compat (↑c.snd) y ∧ A ⟨τ.target, ⟨y, hy⟩⟩) ∨ ∃ τ ∈ temps c.fst false, τ.guard.Realize ↑c.snd ∧ ∃ (y : ι τ.target → M) (hy : (I.domain τ.target).Realize y), τ.Compat (↑c.snd) y ∧ ¬A ⟨τ.target, ⟨y, hy⟩⟩

In a CNF structure interpreted by templates, an assignment satisfies a clause when a template of a polarity applies to its coordinates and relates it to a variable with that truth value.

Defining sentences

@[reducible, inline]

abbrev Cslib.Logic.FO.cnf.posSym : (cnf.sum (ESO.varLanguage fun (x : Unit) => 1)).Relations 2

The symbol pos among those of the satisfiability sentence.

@[reducible, inline]

abbrev Cslib.Logic.FO.cnf.negSym : (cnf.sum (ESO.varLanguage fun (x : Unit) => 1)).Relations 2

The symbol neg among those of the satisfiability sentence.

@[reducible, inline]

abbrev Cslib.Logic.FO.cnf.trueSym : (cnf.sum (ESO.varLanguage fun (x : Unit) => 1)).Relations 1

The relation variable S of the satisfiability sentence, the set of true variables.

def Cslib.Logic.FO.cnf.satMatrix : (cnf.sum (ESO.varLanguage fun (x : Unit) => 1)).Sentence

The first-order part of the satisfiability sentence: ∀ c, ∃ x, (pos(c, x) ∧ S x) ∨ (neg(c, x) ∧ ¬ S x).

def Cslib.Logic.FO.cnf.satSentence : ESO.Sentence cnf

The satisfiability sentence ∃ S, ∀ c, ∃ x, (pos(c, x) ∧ S x) ∨ (neg(c, x) ∧ ¬ S x).

theorem Cslib.Logic.FO.cnf.realize_satSentence {M : Type u_1} [cnf.Structure M] : satSentence.Realize M ↔ Satisfiable M

The satisfiability sentence holds exactly in the satisfiable CNF structures.

theorem Cslib.Logic.FO.cnf.definable_SAT : ESO.Definable SAT

SAT is existential second-order definable.

noncomputable def Cslib.Logic.FO.cnf.fourLiteralsFormula (bs : Fin 4 → Bool) : cnf.Formula (Unit ⊕ Fin 4)

The formula in the variables c (Sum.inl ()) and x₀, …, x₃ (Sum.inr i) saying that the literals (bs i, x i) of the clause c are distinct.

noncomputable def Cslib.Logic.FO.cnf.threeCNFSentence : cnf.Sentence

The 3-CNF sentence: no clause has four distinct literals.

theorem Cslib.Logic.FO.cnf.realize_threeCNFSentence {M : Type u_1} [cnf.Structure M] : M ⊨ threeCNFSentence ↔ IsThreeCNF M

The 3-CNF sentence holds exactly in the 3-CNF structures.

def Cslib.Logic.FO.cnf.nonemptyClausesSentence : cnf.Sentence

The sentence saying that no clause is empty: ∀ c, ∃ x, pos(c, x) ∨ neg(c, x).

theorem Cslib.Logic.FO.cnf.realize_nonemptyClausesSentence {M : Type u_1} [cnf.Structure M] : M ⊨ nonemptyClausesSentence ↔ ∀ (c : M), (literals c).Nonempty

The sentence nonemptyClausesSentence holds exactly when no clause is empty.

theorem Cslib.Logic.FO.cnf.definable_isThreeCNF : Definable {M : CategoryTheory.Bundled cnf.Structure | IsThreeCNF ↑M}

3-CNF structures form a first-order definable class.

theorem Cslib.Logic.FO.cnf.definable_ThreeSAT : ESO.Definable ThreeSAT

3SAT is existential second-order definable.

Encoded CNF structures

def Cslib.Logic.FO.cnf.vocabulary : Vocabulary cnf

The vocabulary of encoded CNF structures: the table of pos, then that of neg.