Maximum cut

AbbreviationInstances of MAXIMUM CUT#✓fully proved

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

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

Used by 3

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

DefinitionWell-formed MAXIMUM CUT instances#✓fully proved

An instance \((n, E, K)\) of MAXIMUM 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 : MaxCutInstance) : 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 CUT

Used byMAXIMUM CUT as a decision problem

DefinitionFeasible MAXIMUM CUT instances#✓fully proved

An instance \((n, E, K)\) of MAXIMUM CUT is feasible when there are a finite set \(S\) of natural numbers, all less than \(n\), and a list \(C\) of length at least \(K\) obtained from \(E\) by deleting zero or more of its entries, such that every pair \((u, v)\) in \(C\) has exactly one of \(u\) and \(v\) in \(S\).

def MaxCutFeasible
    (i : MaxCutInstance) : Prop :=
  ∃ S : Finset ℕ, (∀ v ∈ S, v < i.1) ∧
    ∃ cut : List (ℕ × ℕ), cut.Sublist i.2.1 ∧ i.2.2 ≤ cut.length ∧
      ∀ e ∈ cut, (e.1 ∈ S ∧ e.2 ∉ S) ∨ (e.1 ∉ S ∧ e.2 ∈ S)

Uses 1 · Used by 1

Statement usesInstances of MAXIMUM CUT

Used byMAXIMUM CUT as a decision problem

DefinitionMAXIMUM CUT as a decision problem#✓fully proved

The decision problem MAXIMUM CUT accepts a bitstring \(x\) exactly when decoding \(x\) with the canonical bitstring encoding of instances of MAXIMUM 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 maxCutDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MaxCutInstance) x with
  | some i => decide (WellFormed i ∧ MaxCutFeasible 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 CUT instances · Instances of MAXIMUM CUT · Well-formed MAXIMUM CUT instances · Decision problems

Used byMAXIMUM CUT is NP-complete

TheoremMAXIMUM CUT is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), MAXIMUM CUT.

Uses 5

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