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

theorem DescriptiveComplexity.TDMRed.tPt_surj {A : Type} (q : tdmInterp.Map A) :

∃ (t : TTag) (w : Fin 2 → A), q = tPt t w

Dependency graph

theorem DescriptiveComplexity.TDMRed.tPt_eq_iff {A : Type} {t t' : TTag} {w w' : Fin 2 → A} :

tPt t w = tPt t' w' ↔ t = t' ∧ w = w'

Dependency graph

theorem DescriptiveComplexity.TDMRed.tuple₂_ext {A : Type} {w w' : Fin 2 → A} (h0 : w 0 = w' 0) (h1 : w 1 = w' 1) :

w = w'

Two 2-tuples with the same coordinates are equal.

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

theorem DescriptiveComplexity.TDMRed.tTip_eq_iff {A : Type} {s σ s' σ' : Bool} {x c x' c' : A} :

tTip s σ x c = tTip s' σ' x' c' ↔ s = s' ∧ σ = σ' ∧ x = x' ∧ c = c'

Dependency graph

theorem DescriptiveComplexity.TDMRed.tAv_eq_iff {A : Type} {s s' : Bool} {x c x' c' : A} :

tAv s x c = tAv s' x' c' ↔ s = s' ∧ x = x' ∧ c = c'

Dependency graph

theorem DescriptiveComplexity.TDMRed.tBv_eq_iff {A : Type} {s s' : Bool} {x c x' c' : A} :

tBv s x c = tBv s' x' c' ↔ s = s' ∧ x = x' ∧ c = c'

Dependency graph

theorem DescriptiveComplexity.TDMRed.tGy_eq_iff {A : Type} {s s' : Bool} {x c x' c' : A} :

tGy s x c = tGy s' x' c' ↔ s = s' ∧ x = x' ∧ c = c'

Dependency graph

theorem DescriptiveComplexity.TDMRed.tGz_eq_iff {A : Type} {s s' : Bool} {x c x' c' : A} :

tGz s x c = tGz s' x' c' ↔ s = s' ∧ x = x' ∧ c = c'

Dependency graph

theorem DescriptiveComplexity.TDMRed.tCz_eq_iff {A : Type} {a₀ c c' : A} :

tCz a₀ c = tCz a₀ c' ↔ c = c'

Dependency graph

theorem DescriptiveComplexity.TDMRed.tCy_eq_iff {A : Type} {a₀ c c' : A} :

tCy a₀ c = tCy a₀ c' ↔ c = c'

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

theorem DescriptiveComplexity.TDMRed.tsX_shape {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {q : tdmInterp.Map A} (h : TSXEl q) :

∃ (s : Bool) (σ : Bool) (x : A) (c : A), SatOcc.OccIn c x s ∧ q = tTip s σ x c

Every element of the first class is a tip.

Dependency graph

theorem DescriptiveComplexity.TDMRed.tsY_shape {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {q : tdmInterp.Map A} (h : TSYEl q) :

(∃ (s : Bool) (x : A) (c : A), SatOcc.OccIn c x s ∧ q = tAv s x c) ∨ (∃ (c : A), SatOcc.IsCl c ∧ q = tCy a₀ c) ∨ ∃ (s : Bool) (x : A) (c : A), SatOcc.Chained c x s ∧ q = tGy s x c

Every element of the second class is one of the three kinds.

Dependency graph

theorem DescriptiveComplexity.TDMRed.tsZ_shape {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {q : tdmInterp.Map A} (h : TSZEl q) :

(∃ (s : Bool) (x : A) (c : A), SatOcc.OccIn c x s ∧ q = tBv s x c) ∨ (∃ (c : A), SatOcc.IsCl c ∧ q = tCz a₀ c) ∨ ∃ (s : Bool) (x : A) (c : A), SatOcc.Chained c x s ∧ q = tGz s x c

Every element of the third class is one of the three kinds.

Dependency graph

The triples #

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

TSTrip (tTip s true x c) (tAv s x c) (tBv s x c)

The triple of the truth-setting gadget that frees the false-tip.

Dependency graph

theorem DescriptiveComplexity.TDMRed.tsTrip_wheelF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {s t : Bool} {x c c' : A} (h : SatOcc.VarNext x c s c' t) :

TSTrip (tTip s false x c) (tAv t x c') (tBv s x c)

The triple of the truth-setting gadget that frees the true-tip: it carries the Y-element of the next occurrence of the variable.

Dependency graph

theorem DescriptiveComplexity.TDMRed.tsTrip_clause {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {s : Bool} {x c : A} (h : SatOcc.OccIn c x s) :

TSTrip (tTip s (!s) x c) (tCy a₀ c) (tCz a₀ c)

The triple of a clause, hanging on the tip of one of its occurrences.

Dependency graph

theorem DescriptiveComplexity.TDMRed.tsTrip_garbage {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {s σ t : Bool} {x c x' c' : A} (h : SatOcc.OccIn c x s) (h' : SatOcc.Chained c' x' t) :

TSTrip (tTip s σ x c) (tGy t x' c') (tGz t x' c')

A garbage triple: any tip together with any garbage pair.

Dependency graph

theorem DescriptiveComplexity.TDMRed.tsTrip_bv_inv {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {s : Bool} {x c : A} {p q : tdmInterp.Map A} (h : TSTrip p q (tBv s x c)) :

p = tTip s true x c ∧ q = tAv s x c ∧ SatOcc.OccIn c x s ∨ ∃ (c' : A) (t : Bool), SatOcc.VarNext x c s c' t ∧ p = tTip s false x c ∧ q = tAv t x c'

What can cover a b-element: only the two triples of the truth-setting gadget of its own occurrence.

Dependency graph

theorem DescriptiveComplexity.TDMRed.tsTrip_av_inv {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {s : Bool} {x c : A} {p r : tdmInterp.Map A} (h : TSTrip p (tAv s x c) r) :

p = tTip s true x c ∧ r = tBv s x c ∧ SatOcc.OccIn c x s ∨ ∃ (c₀ : A) (s₀ : Bool), SatOcc.VarNext x c₀ s₀ c s ∧ p = tTip s₀ false x c₀ ∧ r = tBv s₀ x c₀

What can cover an a-element: the gadget triple of its own occurrence, or the one of the occurrence before it.

Dependency graph

theorem DescriptiveComplexity.TDMRed.tsTrip_cy_inv {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {c : A} {p r : tdmInterp.Map A} (h : TSTrip p (tCy a₀ c) r) :

∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ p = tTip s (!s) x c ∧ r = tCz a₀ c

What can cover the Y-element of a clause: only a triple hanging on the tip of one of its occurrences.

Dependency graph

From a matching to an assignment #

def DescriptiveComplexity.TDMRed.WheelTrue {A : Type} (M : tdmInterp.Map A → tdmInterp.Map A → tdmInterp.Map A → Prop) (x c : A) (s : Bool) :

The truth-setting gadget of x uses, at the occurrence (c, s), the triple that frees the false-tip.

Equations

DescriptiveComplexity.TDMRed.WheelTrue M x c s = M (DescriptiveComplexity.TDMRed.tTip s true x c) (DescriptiveComplexity.TDMRed.tAv s x c) (DescriptiveComplexity.TDMRed.tBv s x c)

Instances For

Dependency graph

theorem DescriptiveComplexity.TDMRed.wheel_other {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {M : tdmInterp.Map A → tdmInterp.Map A → tdmInterp.Map A → Prop} (hM : IsMatchingOn TSXEl TSYEl TSZEl TSTrip M) {x c : A} {s : Bool} (hocc : SatOcc.OccIn c x s) (hn : ¬WheelTrue M x c s) :

∃ (c' : A) (t : Bool), SatOcc.VarNext x c s c' t ∧ M (tTip s false x c) (tAv t x c') (tBv s x c)

One triple per occurrence: the gadget of x either frees the false-tip of (c, s) or the true one.

Dependency graph

theorem DescriptiveComplexity.TDMRed.wheel_step {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {M : tdmInterp.Map A → tdmInterp.Map A → tdmInterp.Map A → Prop} (hM : IsMatchingOn TSXEl TSYEl TSZEl TSTrip M) {x c₀ c : A} {s₀ s : Bool} (hnext : SatOcc.VarNext x c₀ s₀ c s) :

WheelTrue M x c s ↔ WheelTrue M x c₀ s₀

The gadget is consistent: neighbouring occurrences of a variable make the same choice.

Dependency graph

theorem DescriptiveComplexity.TDMRed.wheel_const {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {M : tdmInterp.Map A → tdmInterp.Map A → tdmInterp.Map A → Prop} (hM : IsMatchingOn TSXEl TSYEl TSZEl TSTrip M) {x c c' : A} {s s' : Bool} (hocc : SatOcc.OccIn c x s) (hocc' : SatOcc.OccIn c' x s') :

WheelTrue M x c s ↔ WheelTrue M x c' s'

The gadget is a truth value: all the occurrences of a variable make the same choice, since the walk closes into a cycle.

Dependency graph

def DescriptiveComplexity.TDMRed.matchAssign {A : Type} [FirstOrder.Language.sat.Structure A] (M : tdmInterp.Map A → tdmInterp.Map A → tdmInterp.Map A → Prop) (x : A) :

The assignment a matching defines: a variable is true when its gadget frees the false-tips.

Equations

DescriptiveComplexity.TDMRed.matchAssign M x = ∃ (c : A) (s : Bool), DescriptiveComplexity.SatOcc.OccIn c x s ∧ DescriptiveComplexity.TDMRed.WheelTrue M x c s

Instances For

Dependency graph

theorem DescriptiveComplexity.TDMRed.matchAssign_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {M : tdmInterp.Map A → tdmInterp.Map A → tdmInterp.Map A → Prop} (hM : IsMatchingOn TSXEl TSYEl TSZEl TSTrip M) {x c : A} {s : Bool} (hocc : SatOcc.OccIn c x s) :

matchAssign M x ↔ WheelTrue M x c s

Dependency graph

theorem DescriptiveComplexity.TDMRed.matchAssign_sat {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} {M : tdmInterp.Map A → tdmInterp.Map A → tdmInterp.Map A → Prop} (hM : IsMatchingOn TSXEl TSYEl TSZEl TSTrip M) (ha₀ : IsBot a₀) {c : A} (hc : SatOcc.IsCl c) :

∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue (matchAssign M) x s

A matching satisfies every clause: covering the pair of a clause takes the tip of one of its occurrences, and that tip is free exactly when the literal is true.

Dependency graph

From an assignment to a matching #

def DescriptiveComplexity.TDMRed.gbMap {A : Type} [LinearOrder A] (ch fst : A → A × Bool) (c x : A) (s : Bool) :

Where the garbage pair of an occurrence goes: to itself, unless it is the first occurrence of its clause, which is sent to the occurrence the clause gadget consumes. This is the bijection between the tips left over and the garbage pairs.

Equations

DescriptiveComplexity.TDMRed.gbMap ch fst c x s = if (x, s) = fst c then ch c else (x, s)

Instances For

Dependency graph

def DescriptiveComplexity.TDMRed.satMatch {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (a₀ : A) (β : A → Bool) (nxt : A × A × Bool → A × Bool) (ch fst : A → A × Bool) :

tdmInterp.Map A → tdmInterp.Map A → tdmInterp.Map A → Prop

The matching an assignment defines: the gadget triples of the side the assignment picks, one triple per clause, and a garbage triple for every tip left over.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.TDMRed.gbMap_chained {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {β : A → Bool} {ch fst : A → A × Bool} (hch : ∀ (c : A), SatOcc.IsCl c → SatOcc.OccIn c (ch c).1 (ch c).2 ∧ β (ch c).1 = (ch c).2) (hfst : ∀ (c : A), (∃ (x : A) (s : Bool), SatOcc.OccIn c x s) → SatOcc.MinOcc c (fst c).1 (fst c).2) {c x : A} {s : Bool} (hocc : SatOcc.OccIn c x s) (hne : (x, s) ≠ ch c) :

SatOcc.Chained c (gbMap ch fst c x s).1 (gbMap ch fst c x s).2

The garbage pair an occurrence is sent to is a genuine one: a non-first occurrence of its clause.

Dependency graph

theorem DescriptiveComplexity.TDMRed.gbMap_inj {A : Type} [LinearOrder A] {ch fst : A → A × Bool} {c x x' : A} {s s' : Bool} (hne : (x, s) ≠ ch c) (hne' : (x', s') ≠ ch c) (h : gbMap ch fst c x s = gbMap ch fst c x' s') :

(x, s) = (x', s')

The garbage map is injective on the tips left over.

Dependency graph

theorem DescriptiveComplexity.TDMRed.gbMap_surj {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ch fst : A → A × Bool} (hfst : ∀ (c : A), (∃ (x : A) (s : Bool), SatOcc.OccIn c x s) → SatOcc.MinOcc c (fst c).1 (fst c).2) {c x' : A} {s' : Bool} (hchained : SatOcc.Chained c x' s') :

∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ (x, s) ≠ ch c ∧ gbMap ch fst c x s = (x', s')

Every garbage pair is used: the map is onto the non-first occurrences.

Dependency graph

theorem DescriptiveComplexity.TDMRed.satMatch_isMatching {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} {β : A → Bool} {nxt : A × A × Bool → A × Bool} {ch fst : A → A × Bool} (hnxt : ∀ (x c : A) (s : Bool), SatOcc.OccIn c x s → SatOcc.VarNext x c s (nxt (x, c, s)).1 (nxt (x, c, s)).2) (hch : ∀ (c : A), SatOcc.IsCl c → SatOcc.OccIn c (ch c).1 (ch c).2 ∧ β (ch c).1 = (ch c).2) (hfst : ∀ (c : A), (∃ (x : A) (s : Bool), SatOcc.OccIn c x s) → SatOcc.MinOcc c (fst c).1 (fst c).2) (ha₀ : IsBot a₀) :

IsMatchingOn TSXEl TSYEl TSZEl TSTrip (satMatch a₀ β nxt ch fst)

The construction is a matching: every marked element is covered exactly once.

Dependency graph

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