Maximum k-cut

AbbreviationInstances of MAXIMUM k-CUT#✓fully proved

An instance of MAXIMUM k-CUT is a quadruple \((n, E, k, K)\) of a natural number \(n\) (the number of vertices), a finite list \(E\) of ordered pairs of natural numbers (the edges), a natural number \(k\) (the number of parts) and a natural number \(K\) (the bound).

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

Used by 3

Used byMAXIMUM k-CUT as a decision problem · Feasible MAXIMUM k-CUT instances · Well-formed MAXIMUM k-CUT instances

DefinitionWell-formed MAXIMUM k-CUT instances#✓fully proved

An instance \((n, E, k, K)\) of MAXIMUM k-CUT 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 occur in \(E\).

def WellFormed (i : MaxKCutInstance) : Prop :=
  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 MAXIMUM k-CUT

Used byMAXIMUM k-CUT as a decision problem

DefinitionFeasible MAXIMUM k-CUT instances#✓fully proved

An instance \((n, E, k, K)\) of MAXIMUM k-CUT is feasible when there are a list \((a_0, \dots, a_{n-1})\) of \(n\) natural numbers, each less than \(k\), and a list \(C\) of length at least \(K\) obtained from \(E\) by deleting zero or more of its entries, such that \(a_u \ne a_v\) for every pair \((u, v)\) in \(C\), where \(a_w\) is read as \(0\) when \(w \ge n\).

def MaxKCutFeasible
    (i : MaxKCutInstance) : Prop :=
  ∃ assign : List ℕ, assign.length = i.1 ∧ (∀ v < i.1, assign.getD v 0 < i.2.2.1) ∧
    ∃ cut : List (ℕ × ℕ), cut.Sublist i.2.1 ∧ i.2.2.2 ≤ cut.length ∧
      ∀ e ∈ cut, assign.getD e.1 0 ≠ assign.getD e.2 0

Uses 1 · Used by 1

Statement usesInstances of MAXIMUM k-CUT

Used byMAXIMUM k-CUT as a decision problem

DefinitionMAXIMUM k-CUT as a decision problem#✓fully proved

The decision problem MAXIMUM k-CUT accepts a bitstring \(x\) exactly when decoding \(x\) with the canonical bitstring encoding of instances of MAXIMUM k-CUT succeeds and yields an instance that is well formed and feasible. All other bitstrings, including those that fail to decode, are rejected.

noncomputable def maxKCutDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MaxKCutInstance) x with
  | some i => decide (WellFormed i ∧ MaxKCutFeasible 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 MAXIMUM k-CUT instances · Instances of MAXIMUM k-CUT · Well-formed MAXIMUM k-CUT instances · Decision problems

Used byMAXIMUM k-CUT is NP-complete

TheoremMAXIMUM k-CUT is NP-complete#●ready to prove

The decision problem MAXIMUM k-CUT lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to MAXIMUM k-CUT.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), MAXIMUM k-CUT (the k = 2 slice is MAX CUT).

Uses 5

Statement usesPolynomial-time many-one reduction · MAXIMUM k-CUT as a decision problem · 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.