3SAT: definition

The problem 3SAT, over the same vocabulary FirstOrder.Language.sat as SAT: a CNF structure is a yes-instance iff every clause has at most three literal occurrences (DescriptiveComplexity.WidthAtMostThree) and the CNF is satisfiable (DescriptiveComplexity.ThreeSatisfiable, bundled as DescriptiveComplexity.ThreeSAT).

Folding the width bound into the yes-instances (rather than into the vocabulary) is what makes 3SAT a decision problem on arbitrary Language.sat-structures; the bound “at most three” is expressed without counting, as: among any four literal occurrences of a clause, two coincide.

The reductions to and from SAT, and NP-completeness, are in DescriptiveComplexity.Problems.ThreeSat.

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

Every clause of a Language.sat-structure has at most three literal occurrences: among any four occurrences of a clause, two coincide (as signed occurrences).

Equations

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

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

A Language.sat-structure is a yes-instance of 3SAT if every clause has at most three literal occurrences and the CNF is satisfiable.

Equations

• DescriptiveComplexity.ThreeSatisfiable A = (DescriptiveComplexity.WidthAtMostThree A ∧ DescriptiveComplexity.Satisfiable A)

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

The width bound is isomorphism-invariant.

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

3-satisfiability is isomorphism-invariant.

def DescriptiveComplexity.ThreeSAT : DecisionProblem FirstOrder.Language.sat

3SAT, as a problem on Language.sat-structures: the same vocabulary as SAT, with the width bound folded into the yes-instances.

Equations

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