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₄.

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

• DescriptiveComplexity.maxCutGuessBlock = { ι := Bool, ιFinite := Bool.instFinite, arity := fun (i : Bool) => match i with | false => 1 | true => 4 }

def DescriptiveComplexity.mcSideRel : maxCutGuessBlock.lang.Relations 1

The symbol of the relation variable holding one side of the cut.

Equations

• DescriptiveComplexity.mcSideRel = ⟨false, DescriptiveComplexity.mcSideRel._proof_1⟩

def DescriptiveComplexity.mcInjRel : maxCutGuessBlock.lang.Relations 4

The symbol of the injection relation variable.

Equations

• DescriptiveComplexity.mcInjRel = ⟨true, DescriptiveComplexity.mcInjRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.mcSOLang : FirstOrder.Language

The vocabulary of the kernel: arc-marked graphs together with the two guessed relation variables.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.mcAdjSym : mcSOLang.Relations 2

The adjacency symbol in the kernel's vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.mcMarkedSym : mcSOLang.Relations 2

The mark symbol in the kernel's vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.mcSideSym : mcSOLang.Relations 1

The cut-side symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.mcSideSym = Sum.inr DescriptiveComplexity.mcSideRel

@[reducible, inline]

abbrev DescriptiveComplexity.mcInjSym : mcSOLang.Relations 4

The injection symbol in the kernel's vocabulary.

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.