Path cover of a digraph

AbbreviationInstances of DIRECTED PATH COVER#✓fully proved

An instance of DIRECTED PATH COVER is a triple \((n, E, K)\), where the natural number \(n\) is the number of vertices, the list \(E\) of ordered pairs of natural numbers lists the directed edges, and the natural number \(K\) bounds the number of paths.

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

Used by 3

Used byDIRECTED PATH COVER as a decision problem · Feasible DIRECTED PATH COVER instances · Well-formed DIRECTED PATH COVER instances

DefinitionDirected adjacency in an edge list#✓fully proved

For a list \(E\) of ordered pairs of natural numbers and natural numbers \(u\) and \(v\), the directed adjacency test of \(E\) at \((u, v)\) is the boolean that is true exactly when the pair \((u, v)\) occurs in \(E\), that is, when \(E\) contains an edge from \(u\) to \(v\).

def DAdj (edges : List (ℕ × ℕ)) (u v : ℕ) : Bool :=
  edges.contains (u, v)

Used by 1

Used byFeasible DIRECTED PATH COVER instances

DefinitionWell-formed DIRECTED PATH COVER instances#✓fully proved

An instance \((n, E, K)\) of DIRECTED PATH COVER is well formed when the edge list \(E\) has no repeated entries and every edge \((a, b)\) in \(E\) satisfies \(a < n\), \(b < n\) and \(a \ne b\).

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

Uses 1 · Used by 1

Statement usesInstances of DIRECTED PATH COVER

Used byDIRECTED PATH COVER as a decision problem

DefinitionFeasible DIRECTED PATH COVER instances#✓fully proved

An instance \((n, E, K)\) of DIRECTED PATH COVER is feasible when there is a list of at most \(K\) paths, each a list of natural numbers, such that every path has no repeated vertex, every vertex on a path is less than \(n\), and whenever \(v\) immediately follows \(u\) on a path the pair \((u, v)\) occurs in \(E\); and such that every vertex \(v < n\) lies on some path, and all paths containing \(v\) are equal.

def DirectedPathCoverFeasible
    (i : DirectedPathCoverInstance) : Prop :=
  ∃ paths : List (List ℕ), paths.length ≤ i.2.2 ∧
    (∀ p ∈ paths, p.Nodup ∧ (∀ v ∈ p, v < i.1) ∧
      ∀ j, j + 1 < p.length → DAdj i.2.1 (p.getD j 0) (p.getD (j + 1) 0)) ∧
    ∀ v < i.1, ∃ p ∈ paths, v ∈ p ∧ ∀ p' ∈ paths, v ∈ p' → p' = p

Uses 2 · Used by 1

Statement usesDirected adjacency in an edge list · Instances of DIRECTED PATH COVER

Used byDIRECTED PATH COVER as a decision problem

DefinitionDIRECTED PATH COVER as a decision problem#✓fully proved

DIRECTED PATH COVER is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an instance \((n, E, K)\) of DIRECTED PATH COVER that is well formed and feasible; bitstrings that do not decode to an instance are rejected.

noncomputable def directedPathCoverDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := DirectedPathCoverInstance) x with
  | some i => decide (WellFormed i ∧ DirectedPathCoverFeasible 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 · Feasible DIRECTED PATH COVER instances · Instances of DIRECTED PATH COVER · Well-formed DIRECTED PATH COVER instances · Decision problems

Used byDIRECTED PATH COVER is NP-complete

TheoremDIRECTED PATH COVER is NP-complete#●ready to prove

The decision problem DIRECTED PATH COVER is in NP, and every decision problem in NP has a polynomial-time many-one reduction to DIRECTED PATH COVER.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), PATH COVER (the K = 1 slice is Hamiltonian path).

Uses 5

Statement usesPolynomial-time many-one reduction · DIRECTED PATH COVER 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.