Weighted maximum cut

MaxCut is the set of MaxCutInstance values (edges, bound) such that some set S of vertices cuts edges of total weight at least bound [Kar72] Garey and Johnson, Problem ND16: an edge crosses the cut when exactly one of its endpoints lies in S. Vertices, weights and the bound are natural numbers in binary (encNat). The edge list is a weighted multigraph of MaxCut.WeightedEdge: parallel edges add their weights and self-loops never cross a cut. Weights may be zero. MaxCut.cutWeight reads the weight of a cut from an encodable edge list, without a vertex type; Cslib.WeightedCut.cutWeight is the corresponding weight for a weight matrix on a Fintype.

Karp's reduction from Partition takes the complete graph on the positions 0, …, n - 1 of the numbers a, with weight a[i] * a[j] on the edge between positions i < j (Partition.toMaxCut). A cut putting numbers of sum x on one side has weight x * (σ - x), where σ = a.sum (Partition.cutWeight_productEdges), and x * (σ - x) ≥ ⌈σ² / 4⌉ holds exactly when 2 * x = σ. The bound is ⌈σ² / 4⌉ = (σ * σ + 3) / 4. All weights are products of two input numbers, so the reduction is polynomial in the binary encoding.

Main definitions

• Cslib.Complexity.MaxCut.WeightedEdge, Cslib.Complexity.MaxCut.encWeightedEdge: weighted edges and their binary encoding.
• Cslib.Complexity.MaxCut.crosses, Cslib.Complexity.MaxCut.cutWeight: edges crossing a cut and the weight of a cut.
• Cslib.Complexity.MaxCutInstance, Cslib.Complexity.encMaxCut, Cslib.Complexity.MaxCut: problem instances, binary encoding and decision set.
• Cslib.Complexity.MaxCut.verifier: a subset verifier selecting the side S of the cut among the endpoints.
• Cslib.Complexity.Partition.productEdges, Cslib.Complexity.Partition.toMaxCut: Karp's reduction.

Main results

• Cslib.Complexity.MaxCut.isVerifier, Cslib.Complexity.MaxCut.mem_NP: MaxCut ∈ NP encMaxCut.
• Cslib.Complexity.mem_Partition_iff_exists_side: a partition is a set of positions holding half of the total sum.
• Cslib.Complexity.Partition.cutWeight_productEdges: a cut of the complete graph has the weight of the product of the two sides.
• Cslib.Complexity.Partition.toMaxCut_mem_iff: correctness of the reduction.
• Cslib.Complexity.polyTimeReducible_Partition_MaxCut, Cslib.Complexity.MaxCut_npHard, Cslib.Complexity.MaxCut_npComplete: MaxCut is NP-complete.

References

• M. R. Garey and D. S. Johnson, Computers and Intractability
• R. M. Karp, Reducibility among combinatorial problems

structure Cslib.Complexity.MaxCut.WeightedEdge : Type

A weighted edge between u and v of weight weight.

• u : ℕ

  The first endpoint.

• v : ℕ

  The second endpoint.

• weight : ℕ

  The edge weight.

def Cslib.Complexity.MaxCut.instDecidableEqWeightedEdge.decEq (x✝ x✝¹ : WeightedEdge) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.MaxCut.instDecidableEqWeightedEdge : DecidableEq WeightedEdge

@[instance_reducible]

instance Cslib.Complexity.MaxCut.instReprWeightedEdge : Repr WeightedEdge

def Cslib.Complexity.MaxCut.instReprWeightedEdge.repr : WeightedEdge → ℕ → Std.Format

theorem Cslib.Complexity.MaxCut.encWeightedEdge_weight_inO : Turing.MultiTapeTM.ComputableInO WeightedEdge.weight encWeightedEdge Turing.MultiTapeTM.encNat (fun (a : WeightedEdge) => (encWeightedEdge a).length) fun (a : WeightedEdge) => (encWeightedEdge a).length

theorem Cslib.Complexity.MaxCut.encWeightedEdge_u_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → WeightedEdge} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encWeightedEdge S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).u) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.MaxCut.encWeightedEdge_u_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → WeightedEdge} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encWeightedEdge → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).u) encIn✝ Turing.MultiTapeTM.encNat

def Cslib.Complexity.MaxCut.encWeightedEdge : WeightedEdge ↪ List Bool

Weighted edges are encoded as (u, v, weight) in binary.

theorem Cslib.Complexity.MaxCut.encWeightedEdge_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 x1 x2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encNat) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { u := x0 x, v := x1 x, weight := x2 x }) encIn encWeightedEdge

@[simp]

theorem Cslib.Complexity.MaxCut.encWeightedEdge_apply (a : WeightedEdge) : encWeightedEdge a = encWeightedEdgeFields (a.u, a.v, a.weight)

theorem Cslib.Complexity.MaxCut.encWeightedEdge_u_deg : Turing.MultiTapeTM.ComputableInDegree WeightedEdge.u encWeightedEdge Turing.MultiTapeTM.encNat 1 1

@[reducible, inline]

abbrev Cslib.Complexity.MaxCut.encWeightedEdgeFields : ℕ × ℕ × ℕ ↪ List Bool

The tuple of the fields of encWeightedEdge.

theorem Cslib.Complexity.MaxCut.encWeightedEdge_weight_deg : Turing.MultiTapeTM.ComputableInDegree WeightedEdge.weight encWeightedEdge Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.MaxCut.encWeightedEdge_v_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → WeightedEdge} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encWeightedEdge S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).v) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.MaxCut.encWeightedEdge_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : WeightedEdge) => (a.u, a.v, a.weight)) encWeightedEdge encWeightedEdgeFields 1 1

theorem Cslib.Complexity.MaxCut.encWeightedEdge_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 x1 T1 S1 x2 T2 S2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encNat T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn Turing.MultiTapeTM.encNat T2 S2) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { u := x0 x, v := x1 x, weight := x2 x }) encIn encWeightedEdge (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

theorem Cslib.Complexity.MaxCut.encWeightedEdge_v_deg : Turing.MultiTapeTM.ComputableInDegree WeightedEdge.v encWeightedEdge Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.MaxCut.encWeightedEdge_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 x1 x2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encNat budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { u := x0 x, v := x1 x, weight := x2 x }) encIn encWeightedEdge budget

theorem Cslib.Complexity.MaxCut.encWeightedEdge_v_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → WeightedEdge} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encWeightedEdge → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).v) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.MaxCut.encWeightedEdge_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : ℕ × ℕ × ℕ) => { u := p.1, v := p.2.1, weight := p.2.2 }) encWeightedEdgeFields encWeightedEdge 1 1

theorem Cslib.Complexity.MaxCut.encWeightedEdge_weight_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → WeightedEdge} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encWeightedEdge S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).weight) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.MaxCut.encWeightedEdge_u_inO : Turing.MultiTapeTM.ComputableInO WeightedEdge.u encWeightedEdge Turing.MultiTapeTM.encNat (fun (a : WeightedEdge) => (encWeightedEdge a).length) fun (a : WeightedEdge) => (encWeightedEdge a).length

theorem Cslib.Complexity.MaxCut.encWeightedEdge_v_inO : Turing.MultiTapeTM.ComputableInO WeightedEdge.v encWeightedEdge Turing.MultiTapeTM.encNat (fun (a : WeightedEdge) => (encWeightedEdge a).length) fun (a : WeightedEdge) => (encWeightedEdge a).length

theorem Cslib.Complexity.MaxCut.encWeightedEdge_weight_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → WeightedEdge} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encWeightedEdge → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).weight) encIn✝ Turing.MultiTapeTM.encNat

def Cslib.Complexity.MaxCut.crosses (side : ℕ → Bool) (e : WeightedEdge) : Bool

Whether the edge e crosses the cut whose sides are given by side.

def Cslib.Complexity.MaxCut.cutWeight (E : List WeightedEdge) (side : ℕ → Bool) : ℕ

The weight of the cut side in the weighted edges E: the total weight of the crossing edges. Parallel edges add their weights; self-loops never cross.

def Cslib.Complexity.MaxCut.endpoints (E : List WeightedEdge) : List ℕ

The endpoints of the weighted edges E, in order and with repetitions.

theorem Cslib.Complexity.MaxCut.cutWeight_append (E F : List WeightedEdge) (side : ℕ → Bool) : cutWeight (E ++ F) side = cutWeight E side + cutWeight F side

theorem Cslib.Complexity.MaxCut.cutWeight_congr {E : List WeightedEdge} {side side' : ℕ → Bool} (h : ∀ v ∈ endpoints E, side v = side' v) : cutWeight E side = cutWeight E side'

The weight of a cut depends only on the sides of the endpoints.

theorem Cslib.Complexity.MaxCut.length_endpoints (E : List WeightedEdge) : (endpoints E).length = 2 * E.length

structure Cslib.Complexity.MaxCutInstance : Type

An instance of weighted maximum cut: a list of weighted edges and a target cut weight bound.

• edges : List MaxCut.WeightedEdge

  The weighted edges of the multigraph.

• bound : ℕ

  The target cut weight bound.

def Cslib.Complexity.instDecidableEqMaxCutInstance.decEq (x✝ x✝¹ : MaxCutInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqMaxCutInstance : DecidableEq MaxCutInstance

def Cslib.Complexity.instReprMaxCutInstance.repr : MaxCutInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instReprMaxCutInstance : Repr MaxCutInstance

theorem Cslib.Complexity.encMaxCut_bound_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → MaxCutInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encMaxCut S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).bound) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.encMaxCut_edges_deg : Turing.MultiTapeTM.ComputableInDegree MaxCutInstance.edges encMaxCut (Turing.MultiTapeTM.encList MaxCut.encWeightedEdge) 1 1

theorem Cslib.Complexity.encMaxCut_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : List MaxCut.WeightedEdge × ℕ) => { edges := p.1, bound := p.2 }) encMaxCutFields encMaxCut 1 1

theorem Cslib.Complexity.encMaxCut_bound_deg : Turing.MultiTapeTM.ComputableInDegree MaxCutInstance.bound encMaxCut Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encMaxCut_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → List MaxCut.WeightedEdge} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn (Turing.MultiTapeTM.encList MaxCut.encWeightedEdge) budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { edges := x0 x, bound := x1 x }) encIn encMaxCut budget

@[reducible, inline]

abbrev Cslib.Complexity.encMaxCutFields : List MaxCut.WeightedEdge × ℕ ↪ List Bool

The tuple of the fields of encMaxCut.

theorem Cslib.Complexity.encMaxCut_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : MaxCutInstance) => (a.edges, a.bound)) encMaxCut encMaxCutFields 1 1

theorem Cslib.Complexity.encMaxCut_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List MaxCut.WeightedEdge} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn (Turing.MultiTapeTM.encList MaxCut.encWeightedEdge)) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { edges := x0 x, bound := x1 x }) encIn encMaxCut

theorem Cslib.Complexity.encMaxCut_edges_inO : Turing.MultiTapeTM.ComputableInO MaxCutInstance.edges encMaxCut (Turing.MultiTapeTM.encList MaxCut.encWeightedEdge) (fun (a : MaxCutInstance) => (encMaxCut a).length) fun (a : MaxCutInstance) => (encMaxCut a).length

theorem Cslib.Complexity.encMaxCut_bound_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → MaxCutInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encMaxCut → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).bound) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encMaxCut_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List MaxCut.WeightedEdge} {T0 S0 x1 T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn (Turing.MultiTapeTM.encList MaxCut.encWeightedEdge) T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { edges := x0 x, bound := x1 x }) encIn encMaxCut (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encMaxCut_edges_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → MaxCutInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encMaxCut S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).edges) encIn✝ (Turing.MultiTapeTM.encList MaxCut.encWeightedEdge) S✝

theorem Cslib.Complexity.encMaxCut_edges_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → MaxCutInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encMaxCut → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).edges) encIn✝ (Turing.MultiTapeTM.encList MaxCut.encWeightedEdge)

theorem Cslib.Complexity.encMaxCut_bound_inO : Turing.MultiTapeTM.ComputableInO MaxCutInstance.bound encMaxCut Turing.MultiTapeTM.encNat (fun (a : MaxCutInstance) => (encMaxCut a).length) fun (a : MaxCutInstance) => (encMaxCut a).length

def Cslib.Complexity.encMaxCut : MaxCutInstance ↪ List Bool

Instances of MaxCut are encoded as the framed list of weighted edges followed by the bound, all in binary.

@[simp]

theorem Cslib.Complexity.encMaxCut_apply (a : MaxCutInstance) : encMaxCut a = encMaxCutFields (a.edges, a.bound)

def Cslib.Complexity.MaxCut : Set MaxCutInstance

Weighted maximum cut [Kar72]: the weighted edges edges have a cut of weight at least bound, a set S of vertices such that the edges with exactly one endpoint in S have total weight at least bound.

def Cslib.Complexity.MaxCut.check (x : MaxCutInstance) (S : List ℕ) : Bool

The check of a side S of a cut, given as a list: the cut has weight at least the bound.

def Cslib.Complexity.MaxCut.verifier : MaxCutInstance × List Bool → Bool

The verifier for MaxCut, a subset verifier (Cslib.Complexity.subsetVerifier): select the side of the cut among the endpoints and check the weight of the cut.

theorem Cslib.Complexity.MaxCut.computableInPolyTime_check : Turing.MultiTapeTM.ComputableInPolyTime (Function.uncurry check) (Turing.MultiTapeTM.encPair encMaxCut (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encBool

The check of a side of a cut is polynomial-time.

theorem Cslib.Complexity.MaxCut.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encMaxCut Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The MaxCut verifier is polynomial-time.

theorem Cslib.Complexity.MaxCut.mem_MaxCut_iff_endpoints {x : MaxCutInstance} : x ∈ MaxCut ↔ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ endpoints x.edges) ∧ x.bound ≤ cutWeight x.edges fun (v : ℕ) => decide (v ∈ S)

A side of a cut may be taken among the endpoints.

theorem Cslib.Complexity.MaxCut.isVerifier : IsVerifier encMaxCut (2 * Polynomial.X) verifier MaxCut

MaxCut.verifier verifies MaxCut with certificates of twice the length of the encoded instance.

theorem Cslib.Complexity.MaxCut.mem_NP : MaxCut ∈ NP encMaxCut

MaxCut belongs to NP.

theorem Cslib.Complexity.mem_Partition_iff_exists_side {a : List ℕ} : a ∈ Partition ↔ ∃ (side : ℕ → Bool), 2 * (List.map (fun (x : ℕ) => a.getD x 0) (List.filter side (List.range a.length))).sum = a.sum

A partition is a set of positions holding half of the total sum.

def Cslib.Complexity.Partition.productEdges (a : List ℕ) (n : ℕ) : List MaxCut.WeightedEdge

The weighted edges of the complete graph on the positions 0, …, n - 1 of the numbers a: the edge between positions i < j has weight a[i] * a[j].

def Cslib.Complexity.Partition.toMaxCut (a : List ℕ) : MaxCutInstance

Karp's reduction from Partition to MaxCut [Kar72]: the complete graph on the positions of the numbers a, weighted by products, with bound ⌈a.sum² / 4⌉.

theorem Cslib.Complexity.Partition.cutWeight_productEdges (a : List ℕ) (side : ℕ → Bool) (n : ℕ) : MaxCut.cutWeight (productEdges a n) side = (List.map (fun (x : ℕ) => a.getD x 0) (List.filter side (List.range n))).sum * (List.map (fun (x : ℕ) => a.getD x 0) (List.filter (fun (i : ℕ) => !side i) (List.range n))).sum

A cut of the complete graph weighted by products has the weight of the product of the sums of its two sides.

theorem Cslib.Complexity.Partition.toMaxCut_mem_iff (a : List ℕ) : toMaxCut a ∈ MaxCut ↔ a ∈ Partition

Correctness of the reduction to MaxCut.

theorem Cslib.Complexity.Partition.computableInPolyTime_toMaxCut : Turing.MultiTapeTM.ComputableInPolyTime toMaxCut (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) encMaxCut

The reduction toMaxCut is computable in polynomial time.

theorem Cslib.Complexity.polyTimeReducible_Partition_MaxCut : PolyTimeReducible (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) encMaxCut Partition MaxCut

Partition reduces to MaxCut in polynomial time.

theorem Cslib.Complexity.MaxCut_npHard : NPHard encMaxCut MaxCut

MaxCut is NP-hard.

theorem Cslib.Complexity.MaxCut_npComplete : NPComplete encMaxCut MaxCut

Weighted maximum cut is NP-complete, with the weights in binary [Kar72].