Minimum equivalent digraph

AbbreviationInstances of MINIMUM EQUIVALENT DIGRAPH#✓fully proved

An instance of MINIMUM EQUIVALENT DIGRAPH is a triple \((n, E, K)\) consisting of a natural number \(n\) (the number of vertices), a finite list \(E\) of ordered pairs of natural numbers (the arcs) and a natural number \(K\) (the bound on the number of arcs).

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

Used by 3

Used byMINIMUM EQUIVALENT DIGRAPH as a decision problem · Feasible MINIMUM EQUIVALENT DIGRAPH instances · Well-formed MINIMUM EQUIVALENT DIGRAPH instances

DefinitionDirected adjacency for MINIMUM EQUIVALENT DIGRAPH#✓fully proved

For a finite list \(E\) of ordered pairs of natural numbers and natural numbers \(u\) and \(v\), the directed adjacency test of \(E\) at \((u, v)\) returns true when the pair \((u, v)\) occurs in \(E\), and false otherwise.

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

Used by 1

Used byBounded reachability in a digraph

DefinitionBounded reachability in a digraph#✓fully proved

Let \(E\) be a finite list of ordered pairs of natural numbers, read as the arcs of a directed graph, and let \(n\), \(u\) and \(v\) be natural numbers. Then \(v\) is reachable from \(u\) within \(n\) steps along \(E\) when there are natural numbers \(w_0, w_1, \dots, w_k\) with \(k \le n\), \(w_0 = u\) and \(w_k = v\) such that \((w_j, w_{j+1})\) occurs in \(E\) for every \(j < k\).

def Reachable (n : ℕ) (E : List (ℕ × ℕ)) (u v : ℕ) : Prop :=
  ∃ path : List ℕ, path.length ≤ n + 1 ∧ path ≠ [] ∧
    path.getD 0 0 = u ∧ path.getD (path.length - 1) 0 = v ∧
    ∀ j, j + 1 < path.length → DAdj E (path.getD j 0) (path.getD (j + 1) 0)

Uses 1 · Used by 1

Statement usesDirected adjacency for MINIMUM EQUIVALENT DIGRAPH

Used byFeasible MINIMUM EQUIVALENT DIGRAPH instances

DefinitionWell-formed MINIMUM EQUIVALENT DIGRAPH instances#✓fully proved

An instance \((n, E, K)\) of MINIMUM EQUIVALENT DIGRAPH is well formed when the list \(E\) has no repeated entries and every pair \((a, b)\) in \(E\) satisfies \(a < n\), \(b < n\) and \(a \ne b\); that is, \(E\) lists distinct arcs without loops between vertices among \(0, \dots, n - 1\).

def WellFormed (i : MinimumEquivalentDigraphInstance) : 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 MINIMUM EQUIVALENT DIGRAPH

Used byMINIMUM EQUIVALENT DIGRAPH as a decision problem

DefinitionFeasible MINIMUM EQUIVALENT DIGRAPH instances#✓fully proved

An instance \((n, E, K)\) of MINIMUM EQUIVALENT DIGRAPH is feasible when some sublist \(F\) of \(E\) (obtained by deleting entries of \(E\)) has at most \(K\) entries and, for all vertices \(u < n\) and \(v < n\), \(v\) is reachable from \(u\) within \(n\) steps along \(E\) if and only if \(v\) is reachable from \(u\) within \(n\) steps along \(F\).

def MinimumEquivalentDigraphFeasible
    (i : MinimumEquivalentDigraphInstance) : Prop :=
  ∃ F : List (ℕ × ℕ), F.Sublist i.2.1 ∧ F.length ≤ i.2.2 ∧
    ∀ u < i.1, ∀ v < i.1, Reachable i.1 i.2.1 u v ↔ Reachable i.1 F u v

Uses 2 · Used by 1

Statement usesInstances of MINIMUM EQUIVALENT DIGRAPH · Bounded reachability in a digraph

Used byMINIMUM EQUIVALENT DIGRAPH as a decision problem

DefinitionMINIMUM EQUIVALENT DIGRAPH as a decision problem#✓fully proved

The decision problem MINIMUM EQUIVALENT DIGRAPH accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an instance of MINIMUM EQUIVALENT DIGRAPH that is well formed and feasible. Bitstrings that do not decode to an instance are rejected.

noncomputable def minimumEquivalentDigraphDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MinimumEquivalentDigraphInstance) x with
  | some i => decide (WellFormed i ∧ MinimumEquivalentDigraphFeasible 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 MINIMUM EQUIVALENT DIGRAPH instances · Instances of MINIMUM EQUIVALENT DIGRAPH · Well-formed MINIMUM EQUIVALENT DIGRAPH instances · Decision problems

Used byMINIMUM EQUIVALENT DIGRAPH is NP-complete

TheoremMINIMUM EQUIVALENT DIGRAPH is NP-complete#●ready to prove

The decision problem MINIMUM EQUIVALENT DIGRAPH belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), MINIMUM EQUIVALENT DIGRAPH; A. V. Aho, M. R. Garey, and J. D. Ullman, "The transitive reduction of a directed graph", SIAM Journal on Computing 1 (1972), 131-137 (distinguishing transitive reduction from the minimum equivalent subgraph and the hardness connection); D. M. Moyles and G. L. Thompson, "An algorithm for finding a minimum equivalent graph of a digraph", Journal of the ACM 16 (1969), 455-460.

Uses 5

Statement usesPolynomial-time many-one reduction · MINIMUM EQUIVALENT DIGRAPH as a decision problem · Complexity classes · Decision problems · The complexity class NP

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.