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.

inductive FirstOrder.Language.tripleSysRel : ℕ → Type

Relation symbols of the language of triple systems.

• 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.

@[instance_reducible]

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

Equations

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

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.

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 }

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

@[reducible, inline]

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

The first-class symbol.

Equations

• FirstOrder.Language.tsX = FirstOrder.Language.tripleSysRel.xEl

@[reducible, inline]

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

The second-class symbol.

Equations

• FirstOrder.Language.tsY = FirstOrder.Language.tripleSysRel.yEl

@[reducible, inline]

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

The third-class symbol.

Equations

• FirstOrder.Language.tsZ = FirstOrder.Language.tripleSysRel.zEl

@[reducible, inline]

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

The triple symbol.

Equations

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

The shorthands of the vocabulary

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

Belonging to the first class.

Equations

• DescriptiveComplexity.TSXEl a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsX ![a]

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

Belonging to the second class.

Equations

• DescriptiveComplexity.TSYEl a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsY ![a]

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

Belonging to the third class.

Equations

• DescriptiveComplexity.TSZEl a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsZ ![a]

def DescriptiveComplexity.TSTrip {A : Type} [FirstOrder.Language.tripleSys.Structure A] (a b c : A) : Prop

Being an available triple.

Equations

• DescriptiveComplexity.TSTrip a b c = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsTrip ![a, b, c]

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.