3-dimensional matching: definition

3-DIMENSIONAL MATCHING (Karp 1972): given three marked classes and a set of triples, one element from each class, is there a set of triples covering every marked element exactly once?

The vocabulary FirstOrder.Language.tripleSys carries three unary marks xEl, yEl, zEl and one ternary relation trip. A yes-instance is one admitting a matching (DescriptiveComplexity.IsMatchingOn): a sub-relation of trip, inside the three classes, that covers each marked element exactly once. Nothing asks the three classes to be disjoint or to exhaust the universe: elements outside them ride along, and the reduction of DescriptiveComplexity.Problems.ThreeDimMatching.Hardness produces disjoint ones anyway.

Perfect matchings force the three classes to have the same size, which is why the problem is the tripartite form of Exact Cover with sets of size three, and why it is the natural source of the exact-cover family.

@[reducible, inline]

abbrev FirstOrder.Language.tsYEl : Language.tripleSys.Relations 1

yEl a: a belongs to the second class.

Equations

• FirstOrder.Language.tsYEl = FirstOrder.Language.tripleSysRel.yEl

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqTripleSysRel {a✝ : ℕ} : DecidableEq (tripleSysRel a✝)

Equations

• FirstOrder.Language.instDecidableEqTripleSysRel = FirstOrder.Language.instDecidableEqTripleSysRel.decEq

@[reducible, inline]

abbrev FirstOrder.Language.tsXEl : Language.tripleSys.Relations 1

xEl a: a belongs to the first class.

Equations

• FirstOrder.Language.tsXEl = FirstOrder.Language.tripleSysRel.xEl

@[reducible, inline]

abbrev FirstOrder.Language.tsTrip : Language.tripleSys.Relations 3

trip a b c: (a, b, c) is one of the available triples.

Equations

• FirstOrder.Language.tsTrip = FirstOrder.Language.tripleSysRel.trip

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

Equations

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

inductive FirstOrder.Language.tripleSysRel : ℕ → Type

The relation symbols of the language.

• xEl : tripleSysRel 1

  xEl a: a belongs to the first class.

• yEl : tripleSysRel 1

  yEl a: a belongs to the second class.

• zEl : tripleSysRel 1

  zEl a: a belongs to the third class.

• trip : tripleSysRel 3

  trip a b c: (a, b, c) is one of the available triples.

@[reducible, inline]

abbrev FirstOrder.Language.tsZEl : Language.tripleSys.Relations 1

zEl a: a belongs to the third class.

Equations

• FirstOrder.Language.tsZEl = FirstOrder.Language.tripleSysRel.zEl

instance FirstOrder.Language.instIsRelationalTripleSys : Language.tripleSys.IsRelational

def FirstOrder.Language.tripleSys : Language

The relational language of triple systems: three marked classes and a ternary relation.

Equations

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

The shorthands of the vocabulary

def DescriptiveComplexity.TSXEl {A : Type} [FirstOrder.Language.tripleSys.Structure A] (a0 : A) : Prop

xEl a: a belongs to the first class.

Equations

• DescriptiveComplexity.TSXEl a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsXEl ![a0]

def DescriptiveComplexity.TSYEl {A : Type} [FirstOrder.Language.tripleSys.Structure A] (a0 : A) : Prop

yEl a: a belongs to the second class.

Equations

• DescriptiveComplexity.TSYEl a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsYEl ![a0]

def DescriptiveComplexity.TSZEl {A : Type} [FirstOrder.Language.tripleSys.Structure A] (a0 : A) : Prop

zEl a: a belongs to the third class.

Equations

• DescriptiveComplexity.TSZEl a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsZEl ![a0]

def DescriptiveComplexity.TSTrip {A : Type} [FirstOrder.Language.tripleSys.Structure A] (a0 a1 a2 : A) : Prop

trip a b c: (a, b, c) is one of the available triples.

Equations

• DescriptiveComplexity.TSTrip a0 a1 a2 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsTrip ![a0, a1, a2]

Matchings

def DescriptiveComplexity.IsMatchingOn {A : Type} (X Y Z : A → Prop) (T M : A → A → A → Prop) : Prop

A matching: a set of triples, taken from T and lying in the three classes, covering every marked element exactly once.

Equations

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

The problem

def DescriptiveComplexity.HasThreeDimMatching (A : Type) [FirstOrder.Language.tripleSys.Structure A] : Prop

A triple system is a yes-instance when some subset of its triples covers each marked element exactly once.

Equations

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

theorem DescriptiveComplexity.hasThreeDimMatching_iso {A B : Type} [FirstOrder.Language.tripleSys.Structure A] [FirstOrder.Language.tripleSys.Structure B] (e : FirstOrder.Language.tripleSys.Equiv A B) : HasThreeDimMatching A ↔ HasThreeDimMatching B

Having a 3-dimensional matching is isomorphism-invariant.

def DescriptiveComplexity.ThreeDimMatching : DecisionProblem FirstOrder.Language.tripleSys

3-DIMENSIONAL MATCHING, as a problem on triple systems: do some of the triples cover every marked element exactly once?

Equations

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