Minimum bisection

AbbreviationInstances of MINIMUM BISECTION#✓fully proved

An instance of MINIMUM BISECTION is a triple \((n, es, K)\) of a natural number \(n\) (the number of vertices), a list \(es\) of pairs of natural numbers (the edge list) and a natural number \(K\) (the bound on the number of crossing edges).

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

Used by 3

Used byThe decision problem MINIMUM BISECTION · Feasible MINIMUM BISECTION instances · Well-formed MINIMUM BISECTION instances

DefinitionWell-formed MINIMUM BISECTION instances#✓fully proved

An instance \((n, es, K)\) of MINIMUM BISECTION is well formed when \(n\) is even, the list \(es\) has no repeated entries, and every entry \((u, v)\) of \(es\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), and \((v, u)\) is not an entry of \(es\).

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

Uses 1 · Used by 1

Statement usesInstances of MINIMUM BISECTION

Used byThe decision problem MINIMUM BISECTION

DefinitionFeasible MINIMUM BISECTION instances#✓fully proved

An instance \((n, es, K)\) of MINIMUM BISECTION is feasible when there is a set \(S \subseteq \{0, \dots, n - 1\}\) with \(\lfloor n / 2 \rfloor\) elements such that no sublist of \(es\) (a list obtained from \(es\) by deleting entries) with \(K + 1\) entries consists only of entries \((u, v)\) with exactly one of \(u\) and \(v\) in \(S\); that is, at most \(K\) entries of \(es\) have exactly one endpoint in \(S\).

def MinBisectionFeasible
    (i : MinBisectionInstance) : Prop :=
  ∃ S : Finset ℕ, (∀ v ∈ S, v < i.1) ∧ S.card = i.1 / 2 ∧
    ¬ ∃ cut : List (ℕ × ℕ), cut.Sublist i.2.1 ∧ cut.length = i.2.2 + 1 ∧
      ∀ e ∈ cut, (e.1 ∈ S ∧ e.2 ∉ S) ∨ (e.1 ∉ S ∧ e.2 ∈ S)

Uses 1 · Used by 1

Statement usesInstances of MINIMUM BISECTION

Used byThe decision problem MINIMUM BISECTION

DefinitionThe decision problem MINIMUM BISECTION#✓fully proved

The decision problem MINIMUM BISECTION accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of instances, to an instance \((n, es, K)\) of MINIMUM BISECTION that is well formed and feasible (its vertices split into two sets of \(n / 2\) vertices with at most \(K\) entries of \(es\) between them). Bitstrings that do not decode are rejected.

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

Used byMINIMUM BISECTION is NP-complete

TheoremMINIMUM BISECTION is NP-complete#●ready to prove

The decision problem MINIMUM BISECTION belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), MINIMUM BISECTION.

Uses 5

Statement usesPolynomial-time many-one reduction · The decision problem MINIMUM BISECTION · Complexity classes · Decision problems · The complexity class NP

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.