Max Cut: the problem

MAX CUT (Karp 1972): is there a set S of vertices such that at least k edges have exactly one endpoint in S? Here, as everywhere in this library, the threshold k is carried by the instance in the unary representation of DescriptiveComplexity.Numbers.Unary – and, since a cut can have quadratically many edges, at arity 2: k is the number of pairs in the marked relation of FirstOrder.Language.markedArcGraph, the vocabulary introduced for Feedback Arc Set and reused here unchanged.

The cut itself is read as a set of ordered pairs (DescriptiveComplexity.CutRel): the pairs (u, v) with u adjacent to v, u inside S and v outside. On a symmetric adjacency relation this counts every cut edge exactly once, which is what makes the threshold comparison the intended one without any division by two.

The problem

def DescriptiveComplexity.CutRel {A : Type} (Adjp : A → A → Prop) (S : A → Prop) (a b : A) : Prop

The cut determined by S, as a relation: a is adjacent to b, a lies inside S and b outside. Reading the cut as a set of ordered pairs of this shape counts every cut edge of a symmetric adjacency relation once.

Equations

• DescriptiveComplexity.CutRel Adjp S a b = (Adjp a b ∧ S a ∧ ¬S b)

def DescriptiveComplexity.MaxCutOn {A : Type} (Adjp Kp : A → A → Prop) : Prop

Some cut is at least as large as the number encoded by the Kp-marked pairs: “some cut has at least k edges”.

Equations

• DescriptiveComplexity.MaxCutOn Adjp Kp = ∃ (S : A → Prop), {p : A × A | Kp p.1 p.2}.ncard ≤ {p : A × A | DescriptiveComplexity.CutRel Adjp S p.1 p.2}.ncard

theorem DescriptiveComplexity.maxCutOn_iff_certificate {A : Type} [Finite A] (Adjp Kp : A → A → Prop) : MaxCutOn Adjp Kp ↔ ∃ (S : A → Prop), Nonempty ({ p : A × A // Kp p.1 p.2 } ↪ { p : A × A // CutRel Adjp S p.1 p.2 })

The max-cut property, with the threshold certified by an injection of the marked pairs into the cut – the shape the second-order definition guesses.

theorem DescriptiveComplexity.MaxCutOn.of_equiv {A B : Type} (u : B ≃ A) {AdjB KB : B → B → Prop} {AdjA KA : A → A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b b' : B), KB b b' ↔ KA (u b) (u b')) (h : MaxCutOn AdjB KB) : MaxCutOn AdjA KA

MaxCutOn transports along an equivalence commuting with the two relations.

theorem DescriptiveComplexity.MaxCutOn.equiv_iff {A B : Type} (u : B ≃ A) {AdjB KB : B → B → Prop} {AdjA KA : A → A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b b' : B), KB b b' ↔ KA (u b) (u b')) : MaxCutOn AdjB KB ↔ MaxCutOn AdjA KA

MaxCutOn transports along an equivalence, iff version.

def DescriptiveComplexity.HasLargeCut (A : Type) [FirstOrder.Language.markedArcGraph.Structure A] : Prop

An arc-marked graph has a cut at least as large as its marked relation. (Finiteness of the universe is part of the property: cardinality thresholds are only meaningful on finite structures.)

Equations

• DescriptiveComplexity.HasLargeCut A = (Finite A ∧ DescriptiveComplexity.MaxCutOn DescriptiveComplexity.MAGAdj DescriptiveComplexity.MAGMarked)

theorem DescriptiveComplexity.hasLargeCut_iso {A B : Type} [FirstOrder.Language.markedArcGraph.Structure A] [FirstOrder.Language.markedArcGraph.Structure B] (e : FirstOrder.Language.markedArcGraph.Equiv A B) : HasLargeCut A ↔ HasLargeCut B

Having a large cut is isomorphism-invariant.

def DescriptiveComplexity.MaxCut : DecisionProblem FirstOrder.Language.markedArcGraph

MAX CUT, as a problem on arc-marked graphs: is there a set of vertices whose cut is at least as large as the marked relation?

Equations

• DescriptiveComplexity.MaxCut = { Holds := fun (A : Type) (inst : FirstOrder.Language.markedArcGraph.Structure A) => DescriptiveComplexity.HasLargeCut A, iso_invariant := ⋯ }