SAT: propositional satisfiability

The problem SAT, as a decision problem on first-order structures. A CNF formula is a FirstOrder.Language.sat-structure: elements are clauses and propositional variables, satIsClause c distinguishes the clauses, and satPosIn c x / satNegIn c x say that the literal x / ¬x occurs in clause c. DescriptiveComplexity.Satisfiable is the usual satisfiability, and DescriptiveComplexity.SAT the bundled decision problem.

SAT is the archetypical NP-complete problem: this is the Cook–Levin theorem (Cook 1971; Levin 1973; DescriptiveComplexity.SAT_NP_complete, in DescriptiveComplexity.Problems.Sat.Hardness). With NP defined as existential-second-order definability (DescriptiveComplexity.Hierarchy), its membership half is the theorem DescriptiveComplexity.sat_sigmaSODefinable proved here – “there is a truth assignment making every clause true” – and its hardness half is the machine-free, Dahlhaus-style (Dahlhaus 1983) generic reduction DescriptiveComplexity.sat_hard_of_sigmaSODefinable of DescriptiveComplexity.Problems.Sat.Hardness. Other problems' NP-completeness proofs derive from it through first-order reductions; see e.g. DescriptiveComplexity.Problems.ThreeColorability.

inductive FirstOrder.Language.satRel : ℕ → Type

Relation symbols of the language of CNF instances.

• isClause : satRel 1

  isClause c: the element c is a clause.

• posIn : satRel 2

  posIn c x: the variable x occurs positively in the clause c.

• negIn : satRel 2

  negIn c x: the variable x occurs negatively in the clause c.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqSatRel {a✝ : ℕ} : DecidableEq (satRel a✝)

Equations

• FirstOrder.Language.instDecidableEqSatRel = FirstOrder.Language.instDecidableEqSatRel.decEq

def FirstOrder.Language.instDecidableEqSatRel.decEq {a✝ : ℕ} (x✝ x✝¹ : satRel a✝) : Decidable (x✝ = x✝¹)

Equations

• FirstOrder.Language.instDecidableEqSatRel.decEq FirstOrder.Language.satRel.isClause FirstOrder.Language.satRel.isClause = isTrue FirstOrder.Language.instDecidableEqSatRel.decEq._proof_1
• FirstOrder.Language.instDecidableEqSatRel.decEq FirstOrder.Language.satRel.posIn FirstOrder.Language.satRel.posIn = isTrue FirstOrder.Language.instDecidableEqSatRel.decEq._proof_2
• FirstOrder.Language.instDecidableEqSatRel.decEq FirstOrder.Language.satRel.posIn FirstOrder.Language.satRel.negIn = isFalse FirstOrder.Language.instDecidableEqSatRel.decEq._proof_3
• FirstOrder.Language.instDecidableEqSatRel.decEq FirstOrder.Language.satRel.negIn FirstOrder.Language.satRel.posIn = isFalse FirstOrder.Language.instDecidableEqSatRel.decEq._proof_4
• FirstOrder.Language.instDecidableEqSatRel.decEq FirstOrder.Language.satRel.negIn FirstOrder.Language.satRel.negIn = isTrue FirstOrder.Language.instDecidableEqSatRel.decEq._proof_5

def FirstOrder.Language.sat : Language

The relational language of CNF instances: a unary predicate singling out clauses, and two binary predicates for positive and negative occurrences of a variable in a clause.

Equations

• FirstOrder.Language.sat = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.satRel }

instance FirstOrder.Language.instIsRelationalSat : Language.sat.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.satIsClause : Language.sat.Relations 1

The symbol for “is a clause”.

Equations

• FirstOrder.Language.satIsClause = FirstOrder.Language.satRel.isClause

@[reducible, inline]

abbrev FirstOrder.Language.satPosIn : Language.sat.Relations 2

The symbol for “occurs positively in”.

Equations

• FirstOrder.Language.satPosIn = FirstOrder.Language.satRel.posIn

@[reducible, inline]

abbrev FirstOrder.Language.satNegIn : Language.sat.Relations 2

The symbol for “occurs negatively in”.

Equations

• FirstOrder.Language.satNegIn = FirstOrder.Language.satRel.negIn

def DescriptiveComplexity.Satisfiable (A : Type) [FirstOrder.Language.sat.Structure A] : Prop

A Language.sat-structure is satisfiable if some assignment of truth values to its elements makes every clause contain a true literal. (Elements that are not variables of the CNF formula may be assigned arbitrarily; they are harmless since no clause mentions them.)

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.satisfiable_iso {A B : Type} [FirstOrder.Language.sat.Structure A] [FirstOrder.Language.sat.Structure B] (e : FirstOrder.Language.sat.Equiv A B) : Satisfiable A ↔ Satisfiable B

Satisfiability is isomorphism-invariant.

def DescriptiveComplexity.SAT : DecisionProblem FirstOrder.Language.sat

SAT, as a problem on Language.sat-structures.

Equations

• DescriptiveComplexity.SAT = { Holds := fun (A : Type) (inst : FirstOrder.Language.sat.Structure A) => DescriptiveComplexity.Satisfiable A, iso_invariant := ⋯ }

SAT is existential second-order definable

SAT is Σ₁-definable in the sense of DescriptiveComplexity.SecondOrder – “there exists a truth assignment (a unary relation) making every clause true”, the inner part being first-order. Since NP is defined as Σ₁-definability, this is the membership half of the Cook–Levin theorem.

def DescriptiveComplexity.satAssignBlock : SOBlock

The single existential block of the Σ₁ definition of SAT: one unary relation variable, the truth assignment.

Equations

• DescriptiveComplexity.satAssignBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 1 }

def DescriptiveComplexity.satNuSym : satAssignBlock.lang.Relations 1

The symbol of the truth-assignment relation variable.

Equations

• DescriptiveComplexity.satNuSym = ⟨(), DescriptiveComplexity.satNuSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.satSOLang : FirstOrder.Language

The vocabulary of the kernel: CNF instances together with the truth-assignment relation variable.

Equations

• DescriptiveComplexity.satSOLang = FirstOrder.Language.sat.sum DescriptiveComplexity.satAssignBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.kIsClSym : satSOLang.Relations 1

The symbol for “is a clause” in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kIsClSym = Sum.inl FirstOrder.Language.satIsClause

@[reducible, inline]

abbrev DescriptiveComplexity.kPosSym : satSOLang.Relations 2

The symbol for “occurs positively in” in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kPosSym = Sum.inl FirstOrder.Language.satPosIn

@[reducible, inline]

abbrev DescriptiveComplexity.kNegSym : satSOLang.Relations 2

The symbol for “occurs negatively in” in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kNegSym = Sum.inl FirstOrder.Language.satNegIn

@[reducible, inline]

abbrev DescriptiveComplexity.kNuSym : satSOLang.Relations 1

The truth-assignment symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.kNuSym = Sum.inr DescriptiveComplexity.satNuSym

noncomputable def DescriptiveComplexity.satKernel : satSOLang.Sentence

The first-order kernel of the Σ₁ definition of SAT: every clause contains a true literal. The universally quantified variable is the clause, the existentially quantified one the literal's variable.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.realize_satKernel {A : Type} [FirstOrder.Language.sat.Structure A] (ρ : satAssignBlock.Assignment A) : A ⊨ satKernel ↔ ∀ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] → ∃ (x : A), (FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ ρ ↑satNuSym fun (x_1 : Fin (satAssignBlock.arity ↑satNuSym)) => x) ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ∧ ¬ρ ↑satNuSym fun (x_1 : Fin (satAssignBlock.arity ↑satNuSym)) => x

Realization of the kernel under an assignment of the truth-assignment variable: every clause contains a true literal. (Reused by the membership proof of HORN-SAT, whose kernel is this one conjoined with the first-order Horn condition.)

theorem DescriptiveComplexity.sat_sigmaSODefinable : SigmaSODefinable 1 SAT

SAT is Σ₁-definable: satisfiability of a CNF structure is expressed by existentially quantifying a truth assignment and checking, in first-order logic, that every clause contains a true literal.