Documentation

DescriptiveComplexity.Problems.ThreeSat.FromSat

SAT reduces to 3SAT by an ordered FO reduction #

The classical clause-splitting reduction, as an ordered first-order reduction – DescriptiveComplexity.sat_ordered_fo_reduction_threeSat : SAT ≤ᶠᵒ[≤] ThreeSAT. Every clause of the input CNF is split along the linear order of its literal occurrences (DescriptiveComplexity.OccurrenceOrder) into a chain of clauses of width at most three, linked by fresh variables.

Concretely, the interpretation (DescriptiveComplexity.SatToThreeSat.satToThreeSat, tags SplitTag, dimension 2) produces, for each occurrence (x, s) of a clause c:

a linking variable (.link s, (c, x)), intended to mean “no occurrence of c strictly before (x, s) is true”;
a clause piece (.piece s, (c, x)) containing the literal (x, s) itself (on the variable copy (.var, (x, x))), the linking variable of the successor occurrence positively (if any), and its own linking variable negatively (if the occurrence is not the first): at most three literals.

For a clause with occurrences ℓ₁ < ⋯ < ℓₖ, this yields the usual chain (ℓ₁ ∨ y₂), (¬y₂ ∨ ℓ₂ ∨ y₃), …, (¬yₖ ∨ ℓₖ). Empty input clauses are copied as empty clauses (.empty, (c, c)), keeping the output unsatisfiable. All other tuples are junk: they are neither clauses nor occur in any clause.

The two halves of correctness are SatToThreeSat.widthAtMostThree_map (the output always satisfies the width promise – each piece has at most three literals, by uniqueness of the successor occurrence) and SatToThreeSat.satisfiable_iff_map (satisfiability is preserved, by the usual chain argument, threaded along the occurrence order).

inductive DescriptiveComplexity.SatToThreeSat.SplitTag :

Tags for the clause-splitting interpretation of 3SAT instances in ordered CNF instances.

var : SplitTag
(.var, (x, x)) is the copy of the propositional variable x.
link (s : Bool) : SplitTag
(.link s, (c, x)) is the fresh linking variable of the occurrence (x, s) of the clause c.
piece (s : Bool) : SplitTag
(.piece s, (c, x)) is the clause piece of the occurrence (x, s) of the clause c.
empty : SplitTag
(.empty, (c, c)) is the copy of the empty clause c.

Instances For

Dependency graph

def DescriptiveComplexity.SatToThreeSat.instDecidableEqSplitTag.decEq (x✝ x✝¹ : SplitTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SatToThreeSat.instDecidableEqSplitTag :

DecidableEq SplitTag

Equations

DescriptiveComplexity.SatToThreeSat.instDecidableEqSplitTag = DescriptiveComplexity.SatToThreeSat.instDecidableEqSplitTag.decEq

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SatToThreeSat.instFintypeSplitTag :

Fintype SplitTag

Equations

DescriptiveComplexity.SatToThreeSat.instFintypeSplitTag = Fintype.ofEquiv (Unit ⊕ Bool ⊕ Bool ⊕ Unit) DescriptiveComplexity.SatToThreeSat.SplitTag.proxyTypeEquiv

Dependency graph

instance DescriptiveComplexity.SatToThreeSat.instNonemptySplitTag :

Nonempty SplitTag

Dependency graph

noncomputable def DescriptiveComplexity.SatToThreeSat.isClauseF :

SplitTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for satIsClause: clause pieces sit on occurrences, empty-clause copies on diagonal pairs carrying an empty clause.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToThreeSat.posInF :

SplitTag → SplitTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for satPosIn: the piece of a positive occurrence contains its literal positively, and every piece contains the linking variable of the successor occurrence (if any) positively.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.SatToThreeSat.posInF x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToThreeSat.negInF :

SplitTag → SplitTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for satNegIn: the piece of a negative occurrence contains its literal negatively, and the piece of a non-first occurrence contains its own linking variable negatively.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.SatToThreeSat.negInF x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatToThreeSat.satToThreeSat :

FOInterpretation SatOcc.satOrd FirstOrder.Language.sat SplitTag 2

The first-order interpretation producing, from an ordered CNF structure, its width-three split.

Equations

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

Instances For

Dependency graph

Characterizations of the interpreted relations #

@[simp]

theorem DescriptiveComplexity.SatToThreeSat.isClause_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : SplitTag) (w : Fin 2 → A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![(t, w)] ↔ (∃ (s : Bool), t = SplitTag.piece s ∧ SatOcc.OccIn (w 0) (w 1) s) ∨ t = SplitTag.empty ∧ w 0 = w 1 ∧ SatOcc.EmptyCl (w 0)

Dependency graph

@[simp]

theorem DescriptiveComplexity.SatToThreeSat.posIn_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t₁ t₂ : SplitTag) (w₁ w₂ : Fin 2 → A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![(t₁, w₁), (t₂, w₂)] ↔ t₁ = SplitTag.piece true ∧ t₂ = SplitTag.var ∧ (w₂ 0 = w₂ 1 ∧ w₂ 0 = w₁ 1) ∧ SatOcc.OccIn (w₁ 0) (w₁ 1) true ∨ ∃ (s : Bool) (t : Bool), t₁ = SplitTag.piece s ∧ t₂ = SplitTag.link t ∧ w₁ 0 = w₂ 0 ∧ SatOcc.SuccOcc (w₁ 0) (w₁ 1) s (w₂ 1) t

Dependency graph

@[simp]

theorem DescriptiveComplexity.SatToThreeSat.negIn_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t₁ t₂ : SplitTag) (w₁ w₂ : Fin 2 → A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![(t₁, w₁), (t₂, w₂)] ↔ t₁ = SplitTag.piece false ∧ t₂ = SplitTag.var ∧ (w₂ 0 = w₂ 1 ∧ w₂ 0 = w₁ 1) ∧ SatOcc.OccIn (w₁ 0) (w₁ 1) false ∨ ∃ (s : Bool), t₁ = SplitTag.piece s ∧ t₂ = SplitTag.link s ∧ (w₁ 0 = w₂ 0 ∧ w₁ 1 = w₂ 1) ∧ SatOcc.Chained (w₁ 0) (w₁ 1) s

Dependency graph

The width bound #

theorem DescriptiveComplexity.SatToThreeSat.widthAtMostThree_map {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] :

WidthAtMostThree (satToThreeSat.Map A)

The interpreted structure always satisfies the width promise of 3SAT: every clause piece has at most three literal occurrences (its own literal, the successor's linking variable – unique by succOcc_right_unique – and its own linking variable), and empty-clause copies have none.

Dependency graph

Preservation of satisfiability #

def DescriptiveComplexity.SatToThreeSat.splitAssign {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) :

SplitTag × (Fin 2 → A) → Prop

The assignment of the interpreted structure induced by an assignment of the input: variable copies follow ν, and the linking variable of an occurrence states that no earlier occurrence of its clause is true.

Equations

DescriptiveComplexity.SatToThreeSat.splitAssign ν (DescriptiveComplexity.SatToThreeSat.SplitTag.var , w) = ν (w 0)
DescriptiveComplexity.SatToThreeSat.splitAssign ν (DescriptiveComplexity.SatToThreeSat.SplitTag.link s, w) = ¬DescriptiveComplexity.SatOcc.PrefixOrStrict ν (w 0) (w 1) s
DescriptiveComplexity.SatToThreeSat.splitAssign ν x✝ = False

Instances For

Dependency graph

theorem DescriptiveComplexity.SatToThreeSat.exists_litTrue_of_map {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {ν' : satToThreeSat.Map A → Prop} (hν' : ∀ (c : satToThreeSat.Map A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] → ∃ (x : satToThreeSat.Map A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ ν' x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ∧ ¬ν' x) {c : A} (hcl : SatOcc.IsCl c) :

∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue (fun (a : A) => ν' (SplitTag.var , fun (x : Fin 2) => a)) x s

The chain argument of the reduction, isolated in the form its not-all-equal variant reuses (DescriptiveComplexity.NaeSatToNaeThreeSat): if an assignment of the split gives every output clause a true literal, then, read on the variable copies, it gives every clause of the input a true literal.

Dependency graph

theorem DescriptiveComplexity.SatToThreeSat.satisfiable_iff_map {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] :

Satisfiable A ↔ Satisfiable (satToThreeSat.Map A)

Correctness of the reduction, satisfiability half: an ordered CNF structure is satisfiable iff its width-three split is.

Dependency graph

theorem DescriptiveComplexity.SatToThreeSat.satisfiable_iff_threeSatisfiable (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] :

Satisfiable A ↔ ThreeSatisfiable (satToThreeSat.Map A)

Correctness of the reduction: an ordered CNF structure is satisfiable iff its width-three split is a yes-instance of 3SAT.

Dependency graph

noncomputable def DescriptiveComplexity.sat_ordered_fo_reduction_threeSat :

OrderedFOReduction SAT ThreeSAT

SAT FO-reduces to 3SAT on ordered structures. The clause-splitting interpretation SatToThreeSat.satToThreeSat, over the ordered expansion of the language of CNF instances, maps a finite CNF structure to a yes-instance of 3SAT iff it is satisfiable. Together with threeSat_fo_reduction_sat, SAT and 3SAT are FO-interreducible.

Equations

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

Instances For

Dependency graph