Max Cut
Lax799700.MaxCut · concepts/Lax799700/MaxCut.lean · lax-799700
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
MAX CUT: is there a set of vertices such that at least edges have exactly one endpoint in ? Since a cut can have quadratically many edges, the threshold is carried at arity two, as the cardinality of a marked binary relation, on the vocabulary Feedback Arc Set uses. The cut is read as a set of ordered pairs (CutRel), adjacent to with inside and outside, which on a symmetric adjacency relation counts every cut edge exactly once. Membership is by an existential second-order definition, hardness by an ordered first-order reduction from NAE-3SAT.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Mathlib.Data.Fintype.EquivFin |
| 2 | import Mathlib.Data.Set.Card |
| 3 | import Mathlib.SetTheory.Cardinal.Finite |
| 4 | import Mathlib.Logic.Equiv.Prod |
| 5 | import Mathlib.ModelTheory.Semantics |
| 6 | import Mathlib.ModelTheory.Complexity |
| 7 | import Mathlib.Tactic.FinCases |
| 8 | import Mathlib.ModelTheory.Syntax |
| 9 | import Lax799700.Feedback |
| 10 | import Lax904597.Classes |
| 11 | import Lax799700.Problems |
| 12 | |
| 13 | /-! |
| 14 | --- |
| 15 | title: Max Cut |
| 16 | type: theorem |
| 17 | --- |
| 18 | MAX CUT: is there a set of vertices such that at least edges have |
| 19 | exactly one endpoint in ? Since a cut can have quadratically many |
| 20 | edges, the threshold is carried at arity two, as the cardinality of a |
| 21 | marked binary relation, on the vocabulary Feedback Arc Set uses. The cut |
| 22 | is read as a set of ordered pairs (CutRel), adjacent to with |
| 23 | inside and outside, which on a symmetric adjacency relation |
| 24 | counts every cut edge exactly once. Membership is by an existential |
| 25 | second-order definition, hardness by an ordered first-order reduction |
| 26 | from NAE-3SAT. |
| 27 | |
| 28 | -/ |
| 29 | |
| 30 | namespace Lax799700.MaxCut |
| 31 | |
| 32 | open Lax799700.Feedback |
| 33 | |
| 34 | open FirstOrder |
| 35 | |
| 36 | open Language Structure |
| 37 | |
| 38 | section Semantics |
| 39 | |
| 40 | variable {A : Type} |
| 41 | |
| 42 | /-- The cut determined by `S`, as a relation: `a` is adjacent to `b`, `a` lies |
| 43 | inside `S` and `b` outside. Reading the cut as a set of ordered pairs of this |
| 44 | shape counts every cut edge of a symmetric adjacency relation once. -/ |
| 45 | def CutRel (Adjp : A → A → Prop) (S : A → Prop) (a b : A) : Prop := |
| 46 | Adjp a b ∧ S a ∧ ¬S b |
| 47 | |
| 48 | /-- Some cut is at least as large as the number encoded by the `Kp`-marked |
| 49 | pairs: “some cut has at least `k` edges”. -/ |
| 50 | def MaxCutOn (Adjp : A → A → Prop) (Kp : A → A → Prop) : Prop := |
| 51 | ∃ S : A → Prop, |
| 52 | {p : A × A | Kp p.1 p.2}.ncard ≤ {p : A × A | CutRel Adjp S p.1 p.2}.ncard |
| 53 | |
| 54 | end Semantics |
| 55 | |
| 56 | section Problem |
| 57 | |
| 58 | /-- An arc-marked graph has a cut at least as large as its marked relation. |
| 59 | (Finiteness of the universe is part of the property: cardinality thresholds |
| 60 | are only meaningful on finite structures.) -/ |
| 61 | def HasLargeCut (A : Type) [markedArcGraph.Structure A] : Prop := |
| 62 | Finite A ∧ MaxCutOn (MAGAdj (A := A)) (MAGMarked (A := A)) |
| 63 | |
| 64 | end Problem |
| 65 | |
| 66 | open Lax904597.Problems Lax904597.Classes Lax799700.Problems |
| 67 | |
| 68 | /-- The property `HasLargeCut` is isomorphism-invariant. -/ |
| 69 | axiom hasLargeCut_iso : ∀ {A B : Type} [Lax799700.Feedback.markedArcGraph.Structure A] [Lax799700.Feedback.markedArcGraph.Structure B], |
| 70 | (A ≃[Lax799700.Feedback.markedArcGraph] B) → (HasLargeCut A ↔ HasLargeCut B) |
| 71 | |
| 72 | /-- The problem MaxCut: does the structure satisfy `HasLargeCut`? -/ |
| 73 | def MaxCut : DecisionProblem Lax799700.Feedback.markedArcGraph := |
| 74 | DecisionProblem.ofPred HasLargeCut |
| 75 | |
| 76 | /-- The yes-instances of MaxCut are exactly the structures satisfying |
| 77 | `HasLargeCut`. -/ |
| 78 | axiom maxCut_iff : ∀ (A : Type) [Lax799700.Feedback.markedArcGraph.Structure A], MaxCut A ↔ HasLargeCut A |
| 79 | |
| 80 | /-- MaxCut is NP-complete. -/ |
| 81 | axiom maxCut_NP_complete : NP.Complete MaxCut |
| 82 | |
| 83 | end Lax799700.MaxCut |
| 84 |
Used by
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments