Partition into triangles

AbbreviationInstances of PARTITION INTO TRIANGLES#✓fully proved

An instance of PARTITION INTO TRIANGLES is a pair consisting of a natural number \(n\), the number of vertices, and a list of pairs of natural numbers, the edges.

abbrev PartitionIntoTrianglesInstance := ℕ × List (ℕ × ℕ)

Used by 4

Used byGraph of a PARTITION INTO TRIANGLES instance · PARTITION INTO TRIANGLES as a decision problem · Partition into triangles · Well-formed PARTITION INTO TRIANGLES instances

DefinitionGraph of a PARTITION INTO TRIANGLES instance#✓fully proved

For an instance consisting of a natural number \(n\) and a list \(E\) of pairs of natural numbers, its graph is the graph of the edge list \(E\) on \(n\) vertices: the simple graph on \(\{0, \dots, n - 1\}\) in which distinct vertices \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) belongs to \(E\). Pairs with an endpoint at least \(n\) contribute no edge.

def Graph (i : PartitionIntoTrianglesInstance) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 i.2

Uses 2 · Used by 1

Statement usesGraph of an edge list · Instances of PARTITION INTO TRIANGLES

Used byPartition into triangles

DefinitionWell-formed PARTITION INTO TRIANGLES instances#✓fully proved

An instance consisting of a natural number \(n\) and a list \(E\) of pairs of natural numbers is well formed when \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin E\).

def WellFormed (i : PartitionIntoTrianglesInstance) : Prop :=
  i.2.Nodup ∧ ∀ e ∈ i.2, e.1 < i.1 ∧ e.2 < i.1 ∧ e.1 ≠ e.2 ∧ (e.2, e.1) ∉ i.2

Uses 1 · Used by 1

Statement usesInstances of PARTITION INTO TRIANGLES

Used byPARTITION INTO TRIANGLES as a decision problem

DefinitionPartition into triangles#✓fully proved

An instance consisting of a natural number \(n\) and a list \(E\) of pairs of natural numbers admits a partition into triangles when the vertex set \(\{0, \dots, n - 1\}\) can be partitioned into sets of three vertices, any two of which are adjacent in the graph of \(E\) on \(n\) vertices.

def PartitionIntoTrianglesFeasible
    (i : PartitionIntoTrianglesInstance) : Prop :=
  ∃ triples : List (List (Fin i.1)), triples.flatten.Perm (List.finRange i.1) ∧
    (∀ t ∈ triples, t.length = 3 ∧ t.Nodup) ∧
    ∀ t ∈ triples, ∀ a ∈ t, ∀ b ∈ t, a ≠ b → (Graph i).Adj a b

Uses 2 · Used by 1

Statement usesGraph of a PARTITION INTO TRIANGLES instance · Instances of PARTITION INTO TRIANGLES

Used byPARTITION INTO TRIANGLES as a decision problem

DefinitionPARTITION INTO TRIANGLES as a decision problem#✓fully proved

The decision problem PARTITION INTO TRIANGLES accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an instance consisting of a natural number \(n\) and a list \(E\) of pairs of natural numbers such that \(E\) has no repeated entries, every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin E\), and the vertex set \(\{0, \dots, n - 1\}\) can be partitioned into sets of three vertices, any two of which are adjacent in the graph of \(E\) on \(n\) vertices. Bitstrings that do not decode to an instance are rejected.

noncomputable def partitionIntoTrianglesDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := PartitionIntoTrianglesInstance) x with
  | some i => decide (WellFormed i ∧ PartitionIntoTrianglesFeasible i)
  | none => false

Uses 12 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Partition into triangles · Instances of PARTITION INTO TRIANGLES · Well-formed PARTITION INTO TRIANGLES instances · Decision problems

Used byPARTITION INTO TRIANGLES is NP-complete

TheoremPARTITION INTO TRIANGLES is NP-complete#●ready to prove

The decision problem PARTITION INTO TRIANGLES lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to PARTITION INTO TRIANGLES.

public theorem_wanted partitionIntoTriangles_npComplete :
    partitionIntoTrianglesDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L partitionIntoTrianglesDec

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), PARTITION INTO TRIANGLES; D. G. Kirkpatrick and P. Hell, "On the complexity of general graph factor problems", SIAM Journal on Computing 12 (1983), 601-609.

Uses 5

Statement usesPolynomial-time many-one reduction · PARTITION INTO TRIANGLES as a decision problem · Complexity classes · Decision problems · The complexity class NP

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.