Partition into paths of length 2

AbbreviationInstances of PARTITION INTO PATHS OF LENGTH 2#✓fully proved

An instance of PARTITION INTO PATHS OF LENGTH 2 is a pair \((n, E)\) of a natural number \(n\), the number of vertices, and a finite list \(E\) of pairs of natural numbers, the edge list.

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

Used by 4

Used byGraph of a PARTITION INTO PATHS OF LENGTH 2 instance · PARTITION INTO PATHS OF LENGTH 2 · Partitions into paths of length 2 · Well-formed PARTITION INTO PATHS OF LENGTH 2 instances

DefinitionGraph of a PARTITION INTO PATHS OF LENGTH 2 instance#✓fully proved

For an instance \((n, E)\), the graph of the instance is the simple graph on the vertex set \(\{0, \dots, n - 1\}\) in which distinct vertices \(u\) and \(v\) are adjacent exactly when \((u, v)\) or \((v, u)\) belongs to \(E\). Pairs in \(E\) with an entry at least \(n\), and pairs \((u, u)\), contribute no edge.

def Graph (i : PartitionIntoP3sInstance) : 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 PATHS OF LENGTH 2

Used byPartitions into paths of length 2

DefinitionWell-formed PARTITION INTO PATHS OF LENGTH 2 instances#✓fully proved

An instance \((n, E)\) is well formed when the list \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), and the reversed pair \((v, u)\) does not belong to \(E\).

def WellFormed (i : PartitionIntoP3sInstance) : 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 PATHS OF LENGTH 2

Used byPARTITION INTO PATHS OF LENGTH 2

DefinitionPartitions into paths of length 2#✓fully proved

An instance \((n, E)\) admits a partition into paths of length 2 when there is a list of triples, each a list of three distinct vertices from \(\{0, \dots, n - 1\}\), such that every vertex occurs exactly once among all the triples taken together, and every triple contains pairwise distinct vertices \(x\), \(y\), \(z\) such that \(x\) is adjacent to \(y\) and \(y\) is adjacent to \(z\) in the graph of the instance.

The path need not be induced: a triple spanning a triangle qualifies.

def PartitionIntoP3sFeasible
    (i : PartitionIntoP3sInstance) : Prop :=
  ∃ triples : List (List (Fin i.1)), triples.flatten.Perm (List.finRange i.1) ∧
    (∀ t ∈ triples, t.length = 3 ∧ t.Nodup) ∧
    ∀ t ∈ triples, ∃ x ∈ t, ∃ y ∈ t, ∃ z ∈ t,
      x ≠ y ∧ y ≠ z ∧ x ≠ z ∧ (Graph i).Adj x y ∧ (Graph i).Adj y z

Uses 2 · Used by 1

Statement usesGraph of a PARTITION INTO PATHS OF LENGTH 2 instance · Instances of PARTITION INTO PATHS OF LENGTH 2

Used byPARTITION INTO PATHS OF LENGTH 2

DefinitionPARTITION INTO PATHS OF LENGTH 2#✓fully proved

The decision problem PARTITION INTO PATHS OF LENGTH 2 accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of instances, to an instance \((n, E)\) that is well formed and admits a partition into paths of length 2. Bitstrings that do not decode to an instance are rejected.

noncomputable def partitionIntoP3sDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := PartitionIntoP3sInstance) x with
  | some i => decide (WellFormed i ∧ PartitionIntoP3sFeasible 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 · Partitions into paths of length 2 · Instances of PARTITION INTO PATHS OF LENGTH 2 · Well-formed PARTITION INTO PATHS OF LENGTH 2 instances · Decision problems

Used byPARTITION INTO PATHS OF LENGTH 2 is NP-complete

TheoremPARTITION INTO PATHS OF LENGTH 2 is NP-complete#●ready to prove

The decision problem PARTITION INTO PATHS OF LENGTH 2 belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), PARTITION INTO PATHS; M. E. Dyer and A. M. Frieze, "On the complexity of partitioning graphs into connected subgraphs", Discrete Applied Mathematics 10 (1985), 139-153.

Uses 5

Statement usesPolynomial-time many-one reduction · PARTITION INTO PATHS OF LENGTH 2 · 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.