Documentation

DescriptiveComplexity.Problems.ThreeDimMatching.Hardness

3-dimensional matching is NP-hard #

The reduction is Karp's, from SATISFIABILITY, with its three families of triples read off the occurrences of the input formula. Write (c, s) for a signed occurrence – the clause c contains the literal (x, s) – and let a tip be one of the two X-elements tip(x, c, s, σ) attached to it.

The truth-setting gadget. For each occurrence of a variable x there is a Y-element a(x, c, s) and a Z-element b(x, c, s), and two triples
```
(tip(x, c, s, true),  a(x, c, s),   b(x, c, s))
(tip(x, c, s, false), a(x, c', t),  b(x, c, s))     (c', t) = next(c, s)
```
where next runs cyclically through the occurrences of x (DescriptiveComplexity.SatOcc.VarNext). Covering every b picks one triple per occurrence, and covering every a then forces the choice to be the same all around the cycle: the gadget is a truth value, and it frees the tips of one side.
The clause gadget. Each clause c has a Y-element and a Z-element of its own, coverable only by a triple (tip(x, c, s, !s), …). That tip is free exactly when the literal (x, s) is true, so covering the clause pair is satisfying the clause.
Garbage collection. The tips left over have to be covered too, by triples pairing any tip with a private Y/Z pair. There must be exactly as many such pairs as there are leftover tips, and that number is #occurrences − #clauses: the pairs are therefore indexed by the occurrences that are not the first of their clause (DescriptiveComplexity.SatOcc.Chained), the same counting trick the reductions to Partition and to job sequencing use for their slack items.

Nothing here bounds the width of a clause, so the source is SAT itself; an empty clause leaves its two elements uncoverable, which is the right answer.

The tags #

inductive DescriptiveComplexity.TDMRed.TTag :

Tags of the reduction: the two tips of an occurrence, the two elements of its truth-setting gadget, the two elements of a clause, and the two elements of a garbage pair.

tip (s σ : Bool) : TTag
The σ-tip of the occurrence (c, s) of x; its tuple is (x, c).
av (s : Bool) : TTag
The Y-element of the occurrence (c, s) of x; its tuple is (x, c).
bv (s : Bool) : TTag
The Z-element of the occurrence (c, s) of x; its tuple is (x, c).
cy : TTag
The Y-element of the clause c; its tuple is (c, ⊥).
cz : TTag
The Z-element of the clause c; its tuple is (c, ⊥).
gy (s : Bool) : TTag
The Y-element of the garbage pair of a non-first occurrence (x, s) of c; its tuple is (x, c).
gz (s : Bool) : TTag
The Z-element of that garbage pair; its tuple is (x, c).

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.TDMRed.instDecidableEqTTag :

DecidableEq TTag

Equations

DescriptiveComplexity.TDMRed.instDecidableEqTTag = DescriptiveComplexity.TDMRed.instDecidableEqTTag.decEq

Dependency graph

def DescriptiveComplexity.TDMRed.instDecidableEqTTag.decEq (x✝ x✝¹ : TTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.TDMRed.instFintypeTTag :

Equations

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

Dependency graph

instance DescriptiveComplexity.TDMRed.instNonemptyTTag :

Dependency graph

The interpretation #

noncomputable def DescriptiveComplexity.TDMRed.minF {α : Type} (x : α) :

SatOcc.satOrd.Formula α

A minimum of the order, as a formula over the ordered expansion of the vocabulary of CNF instances.

Equations

DescriptiveComplexity.TDMRed.minF x = DescriptiveComplexity.botF x

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.TDMRed.realize_minF {α A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : α → A} {x : α} :

(minF x).Realize v ↔ IsBot (v x)

Dependency graph

noncomputable def DescriptiveComplexity.TDMRed.xElF :

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

Defining formula for the first class: the tips of the occurrences.

Equations

DescriptiveComplexity.TDMRed.xElF (DescriptiveComplexity.TDMRed.TTag.tip s σ) = DescriptiveComplexity.SatOcc.occF s (0, 1) (0, 0)
DescriptiveComplexity.TDMRed.xElF x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.TDMRed.yElF :

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

Defining formula for the second class: one element per occurrence, per clause and per non-first occurrence.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.TDMRed.zElF :

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

Defining formula for the third class, mirroring the second.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.TDMRed.tripF :

TTag → TTag → TTag → SatOcc.satOrd.Formula (Fin 3 × Fin 2)

Defining formula for the triples: the two of the truth-setting gadget of each occurrence, one per occurrence of a clause, and one per tip and garbage pair.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.TDMRed.tripF x✝² x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.TDMRed.tdmInterp :

FOInterpretation SatOcc.satOrd FirstOrder.Language.tripleSys TTag 2

The interpretation of a triple system in a CNF structure.

Equations

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

Instances For

Dependency graph

The points of the interpreted structure #

def DescriptiveComplexity.TDMRed.tPt {A : Type} (t : TTag) (w : Fin 2 → A) :

tdmInterp.Map A

The point of tag t over the pair w.

Equations

DescriptiveComplexity.TDMRed.tPt t w = (t, w)

Instances For

Dependency graph

def DescriptiveComplexity.TDMRed.tTip {A : Type} (s σ : Bool) (x c : A) :

tdmInterp.Map A

The σ-tip of the occurrence (c, s) of x.

Equations

DescriptiveComplexity.TDMRed.tTip s σ x c = DescriptiveComplexity.TDMRed.tPt (DescriptiveComplexity.TDMRed.TTag.tip s σ) ![x, c]

Instances For

Dependency graph

def DescriptiveComplexity.TDMRed.tAv {A : Type} (s : Bool) (x c : A) :

tdmInterp.Map A

The second-class element of the occurrence (c, s) of x.

Equations

DescriptiveComplexity.TDMRed.tAv s x c = DescriptiveComplexity.TDMRed.tPt (DescriptiveComplexity.TDMRed.TTag.av s) ![x, c]

Instances For

Dependency graph

def DescriptiveComplexity.TDMRed.tBv {A : Type} (s : Bool) (x c : A) :

tdmInterp.Map A

The third-class element of the occurrence (c, s) of x.

Equations

DescriptiveComplexity.TDMRed.tBv s x c = DescriptiveComplexity.TDMRed.tPt (DescriptiveComplexity.TDMRed.TTag.bv s) ![x, c]

Instances For

Dependency graph

def DescriptiveComplexity.TDMRed.tCy {A : Type} (a₀ c : A) :

tdmInterp.Map A

The second-class element of the clause c.

Equations

DescriptiveComplexity.TDMRed.tCy a₀ c = DescriptiveComplexity.TDMRed.tPt DescriptiveComplexity.TDMRed.TTag.cy ![c, a₀]

Instances For

Dependency graph

def DescriptiveComplexity.TDMRed.tCz {A : Type} (a₀ c : A) :

tdmInterp.Map A

The third-class element of the clause c.

Equations

DescriptiveComplexity.TDMRed.tCz a₀ c = DescriptiveComplexity.TDMRed.tPt DescriptiveComplexity.TDMRed.TTag.cz ![c, a₀]

Instances For

Dependency graph

def DescriptiveComplexity.TDMRed.tGy {A : Type} (s : Bool) (x c : A) :

tdmInterp.Map A

The second-class element of the garbage pair of the occurrence (x, s) of c.

Equations

DescriptiveComplexity.TDMRed.tGy s x c = DescriptiveComplexity.TDMRed.tPt (DescriptiveComplexity.TDMRed.TTag.gy s) ![x, c]

Instances For

Dependency graph

def DescriptiveComplexity.TDMRed.tGz {A : Type} (s : Bool) (x c : A) :

tdmInterp.Map A

The third-class element of that garbage pair.

Equations

DescriptiveComplexity.TDMRed.tGz s x c = DescriptiveComplexity.TDMRed.tPt (DescriptiveComplexity.TDMRed.TTag.gz s) ![x, c]

Instances For

Dependency graph

The three classes #

@[simp]

theorem DescriptiveComplexity.TDMRed.tsX_tip {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s σ : Bool) (x c : A) :

TSXEl (tTip s σ x c) ↔ SatOcc.OccIn c x s

Dependency graph

@[simp]

theorem DescriptiveComplexity.TDMRed.tsY_av {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (x c : A) :

TSYEl (tAv s x c) ↔ SatOcc.OccIn c x s

Dependency graph

@[simp]

theorem DescriptiveComplexity.TDMRed.tsZ_bv {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (x c : A) :

TSZEl (tBv s x c) ↔ SatOcc.OccIn c x s

Dependency graph

@[simp]

theorem DescriptiveComplexity.TDMRed.tsY_cy {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (c : A) :

TSYEl (tCy a₀ c) ↔ SatOcc.IsCl c

Dependency graph

@[simp]

theorem DescriptiveComplexity.TDMRed.tsZ_cz {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (c : A) :

TSZEl (tCz a₀ c) ↔ SatOcc.IsCl c

Dependency graph

@[simp]

theorem DescriptiveComplexity.TDMRed.tsY_gy {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (x c : A) :

TSYEl (tGy s x c) ↔ SatOcc.Chained c x s

Dependency graph

@[simp]

theorem DescriptiveComplexity.TDMRed.tsZ_gz {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (x c : A) :

TSZEl (tGz s x c) ↔ SatOcc.Chained c x s

Dependency graph

The triples #

From a matching to an assignment #

From an assignment to a matching #

Correctness of the reduction #

theorem DescriptiveComplexity.TDMRed.satisfiable_iff_hasThreeDimMatching (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

Satisfiable A ↔ HasThreeDimMatching (tdmInterp.Map A)

Correctness: a CNF structure is satisfiable exactly when the interpreted triple system has a matching.

Dependency graph

noncomputable def DescriptiveComplexity.sat_ordered_fo_reduction_threeDimMatching :

OrderedFOReduction SAT ThreeDimMatching

SAT ordered-FO-reduces to 3-dimensional matching: two tips, a Y and a Z element per occurrence, a pair per clause, and a garbage pair per non-first occurrence. The truth-setting gadget of a variable runs cyclically through its occurrences, so it admits exactly two matchings – the variable's two truth values – and the pair of a clause can only be covered through the tip of a true literal.

Equations

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

Instances For

Dependency graph