Max Cut is in NP

The Σ₁ definition of DescriptiveComplexity.MaxCut: guess one side S of the cut and an injection of the marked pairs into the cut, the injection being a quaternary relation variable since it maps pairs to pairs, exactly as for Feedback Arc Set, and reusing its DescriptiveComplexity.realize_rel₄.

@[reducible, inline]

abbrev DescriptiveComplexity.mcSOLang : FirstOrder.Language

The vocabulary of the kernel: the instance expanded by the block.

Equations

• DescriptiveComplexity.mcSOLang = FirstOrder.Language.markedArcGraph.sum DescriptiveComplexity.maxCutGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.mcSideSym : mcSOLang.Relations 1

The side symbol over the sum.

Equations

• DescriptiveComplexity.mcSideSym = Sum.inr DescriptiveComplexity.mcSideRel

def DescriptiveComplexity.mcInjRel : maxCutGuessBlock.lang.Relations 4

The inj relation variable.

Equations

• DescriptiveComplexity.mcInjRel = ⟨DescriptiveComplexity.MaxCutGuessBlockIx.inj, DescriptiveComplexity.mcInjRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.mcAdjSym : mcSOLang.Relations 2

The adj symbol over the sum.

Equations

• DescriptiveComplexity.mcAdjSym = Sum.inl FirstOrder.Language.magAdj

def DescriptiveComplexity.maxCutGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Max Cut: one side of the cut (unary) and an injection of the marked relation into the cut (quaternary: it maps pairs to pairs).

Equations

• One or more equations did not get rendered due to their size.

inductive DescriptiveComplexity.MaxCutGuessBlockIx : Type

The relation variables of the block.

• side : MaxCutGuessBlockIx

  One side of the cut.

• inj : MaxCutGuessBlockIx

  The injection of the marked relation into the cut.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqMaxCutGuessBlockIx : DecidableEq MaxCutGuessBlockIx

Equations

• DescriptiveComplexity.instDecidableEqMaxCutGuessBlockIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DescriptiveComplexity.mcSideRel : maxCutGuessBlock.lang.Relations 1

The side relation variable.

Equations

• DescriptiveComplexity.mcSideRel = ⟨DescriptiveComplexity.MaxCutGuessBlockIx.side, DescriptiveComplexity.mcSideRel._proof_1⟩

@[instance_reducible]

instance DescriptiveComplexity.instFintypeMaxCutGuessBlockIx : Fintype MaxCutGuessBlockIx

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev DescriptiveComplexity.mcMarkedSym : mcSOLang.Relations 2

The marked symbol over the sum.

Equations

• DescriptiveComplexity.mcMarkedSym = Sum.inl FirstOrder.Language.magMarked

@[reducible, inline]

abbrev DescriptiveComplexity.mcInjSym : mcSOLang.Relations 4

The inj symbol over the sum.

Equations

• DescriptiveComplexity.mcInjSym = Sum.inr DescriptiveComplexity.mcInjRel

noncomputable def DescriptiveComplexity.maxCutKernel : mcSOLang.Sentence

The first-order kernel of the Σ₁ definition of Max Cut.

Equations

• DescriptiveComplexity.maxCutKernel = DescriptiveComplexity.mcTotalClause✝ ⊓ DescriptiveComplexity.mcInjClause✝

theorem DescriptiveComplexity.maxCut_sigmaSODefinable : SigmaSODefinable 1 MaxCut

Max Cut is Σ₁-definable: existentially guess one side of the cut and an injection of the marked relation into the cut – a quaternary relation variable, the threshold being carried by pairs. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Max Cut.