Inapproximability of MAX-CUT

DefinitionVertex count of a MAX-CUT instance#✓fully proved

The vertex count of a MAX-CUT instance, a bitstring \(x\) of length \(|x|\), is \(\lfloor \sqrt{|x|} \rfloor\).

def maxCutN (x : List Bool) : ℕ := Nat.sqrt x.length

Sources

• C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440.

Used by 3

Used byMAX-CUT as an optimization problem · Feasible MAX-CUT solutions · Value of a MAX-CUT solution

DefinitionFeasible MAX-CUT solutions#✓fully proved

A bitstring \(s\) is a feasible solution of a MAX-CUT instance \(x\) exactly when the length of \(s\) equals the vertex count \(\lfloor \sqrt{|x|} \rfloor\) of \(x\), so that \(s\) has one bit per vertex.

def maxCutFeas (x s : List Bool) : Bool := decide (s.length = maxCutN x)

Sources

• C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440.

Uses 1 · Used by 2

Statement usesVertex count of a MAX-CUT instance

Used byMAX-CUT as an optimization problem · Value of a MAX-CUT solution

DefinitionValue of a MAX-CUT solution#✓fully proved

Let \(x\) be a MAX-CUT instance with vertex count \(n = \lfloor \sqrt{|x|} \rfloor\) and let \(s\) be a bitstring, with bits indexed from \(0\). If \(s\) is a feasible solution of \(x\) (its length is \(n\)), the value of \(s\) is the number, as a rational number, of pairs \((i, j)\) with \(i < j < n\) such that bit \(i n + j\) of \(x\) is true and bits \(i\) and \(j\) of \(s\) differ; otherwise the value is \(0\).

def maxCutVal (x s : List Bool) : ℚ :=
  if maxCutFeas x s then
    ((Finset.filter (fun p : ℕ × ℕ => p.1 < p.2 ∧ p.2 < maxCutN x ∧
      x.getD (p.1 * maxCutN x + p.2) false ∧
        (s.getD p.1 false) ≠ (s.getD p.2 false))
      (Finset.range (maxCutN x) ×ˢ Finset.range (maxCutN x))).card : ℚ)
  else 0

Sources

• C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440.

Uses 2 · Used by 1

Statement usesFeasible MAX-CUT solutions · Vertex count of a MAX-CUT instance

Used byMAX-CUT as an optimization problem

DefinitionMAX-CUT as an optimization problem#✓fully proved

MAX-CUT is the optimization problem whose instances are bitstrings \(x\), read as an adjacency matrix on \(n = \lfloor \sqrt{|x|} \rfloor\) vertices in which, for \(i < j < n\), bit \(i n + j\) of \(x\) (bits indexed from \(0\)) says whether \(\{i, j\}\) is an edge. Its feasible solutions for \(x\) are the bitstrings of length \(n\), one bit per vertex; the value of a feasible solution \(s\) is the number of pairs \(i < j < n\) that are edges and whose bits in \(s\) differ, the value of an infeasible solution is \(0\), and the polynomial bound on the length of feasible solutions is \(p(m) = m\).

MetaMathlibExt.Complexity.KeyTheorems.MaxCutNoPTAS.maxCut · 20 lines

noncomputable def maxCut : OptProblem where
  val := maxCutVal
  feas := maxCutFeas
  bound := Polynomial.X
  feas_len := fun x s h => by
    unfold maxCutFeas at h
    rw [decide_eq_true_eq] at h
    rw [h]
    simp [Polynomial.eval_X, maxCutN, Nat.sqrt_le_self]
  val_nonneg := fun x s => by
    unfold maxCutVal
    split
    · exact Nat.cast_nonneg _
    · exact le_rfl
  val_infeas := fun x s h => by
    unfold maxCutVal
    have h' : maxCutFeas x s ≠ true := by rw [h]; exact Bool.false_ne_true
    simp [h']
  feas_nonempty := fun x => ⟨List.replicate (maxCutN x) false, by
    simp [maxCutFeas, List.length_replicate]⟩

Sources

• C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440.

Uses 4 · Used by 1

Statement usesOptimization problems · Feasible MAX-CUT solutions · Vertex count of a MAX-CUT instance · Value of a MAX-CUT solution

Used byMAX-CUT has no PTAS unless P = NP

TheoremMAX-CUT has no PTAS unless P = NP#●ready to prove

If \(\mathsf{P} \neq \mathsf{NP}\), then the optimization problem MAX-CUT does not admit a polynomial-time approximation scheme.

public theorem_wanted max_cut_no_ptas :
    P ≠ NP → ¬ IsPTAS maxCut

Sources

• C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440 (MAX-CUT is MAXSNP-complete, hence APX-hard); S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Chapter 11 (APX-hardness rules out a PTAS unless P = NP).

Uses 5

Statement usesPolynomial-time approximation schemes · MAX-CUT as an optimization problem · Complexity classes · The complexity class NP · The complexity class P

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.