Maximum flow

DefinitionMax-flow decision problem#✓fully proved

The decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a tuple \((n, E, s, t, K)\) of a natural number \(n\), a list \(E = (e_0, \dots, e_{m-1})\) of triples \(e_j = (u_j, v_j, c_j)\) of natural numbers and natural numbers \(s\), \(t\) and \(K\) such that \(u_j < n\), \(v_j < n\) and \(u_j \neq v_j\) for every \(j < m\), \(s < n\), \(t < n\) and \(s \neq t\), and there are natural numbers \(f_0, \dots, f_{m-1}\) with \(f_j \le c_j\) for every \(j < m\), with \(\sum_{j : v_j = v} f_j = \sum_{j : u_j = v} f_j\) for every \(v < n\) other than \(s\) and \(t\), and with \(\sum_{j : u_j = s} f_j - \sum_{j : v_j = s} f_j \ge K\), where the subtraction is truncated at \(0\). Bitstrings that do not decode are rejected.

MetaMathlibExt.Complexity.KeyTheorems.MaxFlowInP.maxFlowDec · 20 lines

noncomputable def maxFlowDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ℕ × List (ℕ × ℕ × ℕ) × ℕ × ℕ × ℕ) x with
  | some i => decide (
      (∀ e ∈ i.2.1, e.1 < i.1 ∧ e.2.1 < i.1 ∧ e.1 ≠ e.2.1) ∧
      i.2.2.1 < i.1 ∧ i.2.2.2.1 < i.1 ∧ i.2.2.1 ≠ i.2.2.2.1 ∧
      ∃ flow : List ℕ, flow.length = i.2.1.length ∧
        (∀ j < i.2.1.length, flow.getD j 0 ≤ (i.2.1.getD j (0, 0, 0)).2.2) ∧
        (∀ v < i.1, v ≠ i.2.2.1 → v ≠ i.2.2.2.1 →
          (Finset.range i.2.1.length).sum (fun j =>
            if (i.2.1.getD j (0, 0, 0)).2.1 = v then flow.getD j 0 else 0) =
          (Finset.range i.2.1.length).sum (fun j =>
            if (i.2.1.getD j (0, 0, 0)).1 = v then flow.getD j 0 else 0)) ∧
        (Finset.range i.2.1.length).sum (fun j =>
          if (i.2.1.getD j (0, 0, 0)).1 = i.2.2.1 then flow.getD j 0 else 0) -
        (Finset.range i.2.1.length).sum (fun j =>
          if (i.2.1.getD j (0, 0, 0)).2.1 = i.2.2.1 then flow.getD j 0 else 0) ≥
            i.2.2.2.2)
  | none => false

Uses 9 · 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 · Decision problems

Used byMax flow is in P (Edmonds-Karp)

TheoremMax flow is in P (Edmonds-Karp)#●ready to prove

The max-flow decision problem belongs to the complexity class P. This is the problem of deciding, for a vertex count \(n\), a list of edges joining distinct vertices below \(n\) with natural-number capacities, distinct vertices \(s, t < n\) and a target \(K\), encoded as a bitstring, whether some flow in natural numbers that respects the capacities and is conserved at every vertex other than \(s\) and \(t\) has net outflow from \(s\) at least \(K\).

public theorem_wanted max_flow_in_p :
    maxFlowDec ∈ MetaMathlibExt.ComplexityTheory.P

Sources

• J. Edmonds and R. M. Karp, "Theoretical improvements in algorithmic efficiency for network flow problems", Journal of the ACM 19 (1972), 248-264; L. R. Ford Jr. and D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.

Uses 4

Statement usesMax-flow decision problem · Complexity classes · Decision problems · The complexity class P

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.