Monotone formulas for bipartite perfect matching need linear depth

Raz and Wigderson showed that monotone circuits deciding whether a graph has a perfect matching need linear depth [RW92]. For bipartite graphs with n left and n right vertices, a monotone formula computing bipartitePerfectMatching n has depth at least (n - 2 ^ 14) / 2 ^ 13 (Monotone.le_mul_eformulaDepth_bipartitePerfectMatching_add). By the monotone Karchmer–Wigderson theorem (Monotone.eformulaDepth_eq_ecomplexity) this is a lower bound on the monotone Karchmer–Wigderson game of bipartite perfect matching (le_mul_ecomplexity_bipartitePerfectMatching_add): Alice holds a graph with a perfect matching, Bob one without, and they must find an edge of Alice's graph missing from Bob's.

The proof is a randomized reduction from disjointness, whose randomized complexity is linear (PublicCoin.le_mul_ecomplexityFun_disjointness_add_of_le), to this game [RW92], Kushilevitz and Nisan, Chapter 10, here with gadgets for bipartite graphs. Let Alice and Bob hold sets x, y ⊆ [m] and fix i₀ ∈ [m]. Every i has a left vertex bᵢ and right vertices aᵢ, cᵢ (RazWigderson.Vertex, with m + e further left vertices and e further right ones to reach n). Alice's graph is a perfect matching that matches bᵢ to aᵢ when i ∈ x and to cᵢ otherwise (RazWigderson.aliceGraph). Bob's graph omits exactly the edges from the vertices bᵢ with i = i₀ or i ∈ y to the right vertices other than the cⱼ with j ≠ i₀ and j ∈ y; the former outnumber the latter by one, so it has no perfect matching (RazWigderson.bobGraph, RazWigderson.not_hasPerfectMatching_bobGraph). The edges of Alice's graph missing from Bob's lie at bᵢ₀ and at the bᵢ with i ∈ x ∩ y (RazWigderson.exists_of_aliceGraph_of_bobGraph). With shared random bits the players relabel the vertices by a uniformly random pair of permutations, run a protocol for the game, and Bob answers that the sets are disjoint when the edge found is at bᵢ₀ and i₀ is not in both sets (RazWigderson.bobAnswer, RazWigderson.oneRun). On disjoint sets the answer is always right. If some ℓ ≠ i₀ is in both sets, exchanging the edges of Alice's matching at bᵢ₀ and bℓ preserves both graphs, so the edge found is at bᵢ₀ for at most half of the relabellings (RazWigderson.two_mul_card_filter_run_oneRun_le). Answering that the sets are disjoint only when k independent runs all say so errs with probability at most 2 ^ (-k), with k (c + 1) bits for a protocol of c bits (RazWigderson.solves_reduction, ecomplexityFun_disjointness_le_mul_ecomplexity_bipartitePerfectMatching). Taking k = 6 and m = n / 2 gives the bound. The constants are not optimized.

Main definitions

• Cslib.Circuits.BipartiteMatching.RazWigderson.aliceGraph, Cslib.Circuits.BipartiteMatching.RazWigderson.bobGraph: the graphs of the reduction.
• Cslib.Circuits.BipartiteMatching.RazWigderson.reduction: the public-coin protocol for disjointness.

Main results

• Cslib.Circuits.BipartiteMatching.RazWigderson.two_mul_card_filter_run_oneRun_le: the symmetry of the reduction.
• Cslib.Circuits.BipartiteMatching.RazWigderson.solves_reduction: its error.
• Cslib.Circuits.ecomplexityFun_disjointness_le_mul_ecomplexity_bipartitePerfectMatching: the Raz–Wigderson reduction.
• Cslib.Circuits.le_mul_ecomplexity_bipartitePerfectMatching_add: the monotone Karchmer–Wigderson game of bipartite perfect matching needs Ω(n) bits.
• Cslib.Circuits.Monotone.le_mul_eformulaDepth_bipartitePerfectMatching_add: monotone formulas for bipartite perfect matching need depth Ω(n).

References

• R. Raz and A. Wigderson, Monotone circuits for matching require linear depth
• E. Kushilevitz and N. Nisan, Communication Complexity

The graphs of the reduction

@[reducible, inline]

abbrev Cslib.Circuits.BipartiteMatching.RazWigderson.Vertex (m e : ℕ) : Type

The vertices of the graphs of the reduction, on each side: two copies of Fin m and e extra vertices. On the left, inl (inl i) is the vertex bᵢ of the gadget of i; on the right, inl (inl i) and inl (inr i) are its vertices aᵢ and cᵢ.

def Cslib.Circuits.BipartiteMatching.RazWigderson.swapIf {m : ℕ} (x : BitString m) : Fin m ⊕ Fin m → Fin m ⊕ Fin m

Exchange inl i and inr i exactly when the bit x i is zero.

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.swapIf_involutive {m : ℕ} (x : BitString m) : Function.Involutive (swapIf x)

Exchanging twice gives back the vertex.

def Cslib.Circuits.BipartiteMatching.RazWigderson.aliceMatching {m e : ℕ} (x : BitString m) : Equiv.Perm (Vertex m e)

Alice's perfect matching: the gadget vertex bᵢ is matched to aᵢ when i is in her set and to cᵢ otherwise, the other copy of Fin m takes the remaining vertices, and the extra vertices are matched to themselves.

@[simp]

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.aliceMatching_inl_inl {m e : ℕ} (x : BitString m) (i : Fin m) : (aliceMatching x) (Sum.inl (Sum.inl i)) = Sum.inl (bif x i then Sum.inl i else Sum.inr i)

Alice matches bᵢ to aᵢ when x i is one and to cᵢ otherwise.

def Cslib.Circuits.BipartiteMatching.RazWigderson.aliceGraph {m e : ℕ} (x : BitString m) (p : Vertex m e × Vertex m e) : Bool

Alice's graph: the edges of her perfect matching.

def Cslib.Circuits.BipartiteMatching.RazWigderson.hallSet {m e : ℕ} (i₀ : Fin m) (y : BitString m) : Vertex m e → Bool

The left vertices of Bob's Hall violator: the gadget vertices bᵢ with i = i₀ or i in his set.

def Cslib.Circuits.BipartiteMatching.RazWigderson.coverSet {m e : ℕ} (i₀ : Fin m) (y : BitString m) : Vertex m e → Bool

Their neighbours in Bob's graph: the gadget vertices cⱼ with j ≠ i₀ in his set.

def Cslib.Circuits.BipartiteMatching.RazWigderson.bobGraph {m e : ℕ} (i₀ : Fin m) (y : BitString m) (p : Vertex m e × Vertex m e) : Bool

Bob's graph: all edges except those from hallSet to right vertices outside coverSet.

def Cslib.Circuits.BipartiteMatching.RazWigderson.bobAnswer {m e : ℕ} (i₀ : Fin m) (y : BitString m) (p : Vertex m e × Vertex m e) : Bool

Bob's answer to an edge found by the Karchmer–Wigderson protocol, true meaning that the sets are disjoint: whether the edge starts at bᵢ₀ and, when i₀ is in his set, ends at cᵢ₀.

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.hasPerfectMatching_aliceGraph {m e : ℕ} (x : BitString m) : HasPerfectMatching (aliceGraph x)

Alice's graph has a perfect matching: her matching.

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.not_hasPerfectMatching_bobGraph {m e : ℕ} (i₀ : Fin m) (y : BitString m) : ¬HasPerfectMatching (bobGraph i₀ y)

Bob's graph has no perfect matching: hallSet has one more vertex than coverSet, which contains all its neighbours.

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.exists_of_aliceGraph_of_bobGraph {m e : ℕ} {x y : BitString m} {i₀ : Fin m} {p : Vertex m e × Vertex m e} (hA : aliceGraph x p = true) (hB : bobGraph i₀ y p = false) : ∃ (i : Fin m), p = (Sum.inl (Sum.inl i), (aliceMatching x) (Sum.inl (Sum.inl i))) ∧ (i = i₀ ∨ x i = true ∧ y i = true)

The edges of Alice's graph missing from Bob's graph are the edges of her matching at bᵢ for i = i₀ and for i in both sets.

The randomized protocol

@[reducible, inline]

abbrev Cslib.Circuits.BipartiteMatching.RazWigderson.Relabeling (m e : ℕ) : Type

The relabellings of the graphs of the reduction: a permutation of the left and one of the right vertices.

@[instance_reducible]

instance Cslib.Circuits.BipartiteMatching.RazWigderson.instFintypeRelabeling (m e : ℕ) : Fintype (Relabeling m e)

The relabellings form a finite type. Declaring the instance directly keeps the instance terms for tuples of relabellings below the size limit of instance synthesis.

def Cslib.Circuits.BipartiteMatching.RazWigderson.relabel {m e n : ℕ} (h : Vertex m e ≃ Fin n) (σ : Relabeling m e) (k : Fin (n * n)) : Vertex m e × Vertex m e

The pair of vertices named by an input bit of bipartitePerfectMatching n, identifying the vertices of the reduction with Fin n along h and relabelling them by σ.

def Cslib.Circuits.BipartiteMatching.RazWigderson.oneRun {m e n : ℕ} (p : Communication.KWProtocol (Fin (n * n))) (h : Vertex m e ≃ Fin n) (i₀ : Fin m) (σ : Relabeling m e) : Communication.Protocol (BitString m) (BitString m) Bool

One run of the reduction: the players relabel their graphs by σ, run the protocol p for the monotone Karchmer–Wigderson game of bipartite perfect matching on them, and Bob answers on the edge it finds.

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.run_oneRun {m e n : ℕ} {p : Communication.KWProtocol (Fin (n * n))} {h : Vertex m e ≃ Fin n} {i₀ : Fin m} (σ : Relabeling m e) (x y : BitString m) : (oneRun p h i₀ σ).run x y = bobAnswer i₀ y (relabel h σ (Communication.Protocol.run p (fun (k : Fin (n * n)) => aliceGraph x (relabel h σ k)) fun (k : Fin (n * n)) => bobGraph i₀ y (relabel h σ k)))

A run outputs Bob's answer on the edge found by p, relabelled back.

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.depth_oneRun_le {m e n : ℕ} {p : Communication.KWProtocol (Fin (n * n))} {h : Vertex m e ≃ Fin n} {i₀ : Fin m} (σ : Relabeling m e) : (oneRun p h i₀ σ).depth ≤ Communication.Protocol.depth p + 1

A run sends one more bit than p.

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.bipartitePerfectMatching_aliceGraph {m e n : ℕ} (h : Vertex m e ≃ Fin n) (σ : Relabeling m e) (x : BitString m) : (bipartitePerfectMatching n fun (k : Fin (n * n)) => aliceGraph x (relabel h σ k)) = true

The relabelled graphs are an instance of the monotone Karchmer–Wigderson game of bipartite perfect matching: Alice's has a perfect matching and Bob's has none.

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.bipartitePerfectMatching_bobGraph {m e n : ℕ} {i₀ : Fin m} (h : Vertex m e ≃ Fin n) (σ : Relabeling m e) (y : BitString m) : (bipartitePerfectMatching n fun (k : Fin (n * n)) => bobGraph i₀ y (relabel h σ k)) = false

Bob's relabelled graph has no perfect matching.

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.two_mul_card_filter_run_oneRun_le {m e n : ℕ} {p : Communication.KWProtocol (Fin (n * n))} {h : Vertex m e ≃ Fin n} {i₀ : Fin m} {x y : BitString m} {ℓ : Fin m} (hℓ : ℓ ≠ i₀) (hx : x ℓ = true) (hy : y ℓ = true) : 2 * {σ : Relabeling m e | (oneRun p h i₀ σ).run x y = true}.card ≤ Fintype.card (Relabeling m e)

The symmetry of the reduction. If some ℓ ≠ i₀ is in both sets, a run answers true for at most half of the relabellings: exchanging the edges of Alice's matching at bᵢ₀ and bℓ preserves both graphs, hence the edge found, but moves it off bᵢ₀ when it was there.

def Cslib.Circuits.BipartiteMatching.RazWigderson.repeatedRun {m e n k : ℕ} (p : Communication.KWProtocol (Fin (n * n))) (h : Vertex m e ≃ Fin n) (i₀ : Fin m) (σs : Fin k → Relabeling m e) : Communication.Protocol (BitString m) (BitString m) Bool

k runs of the reduction with independent relabellings; the answer is that the sets are disjoint when every run says so.

noncomputable def Cslib.Circuits.BipartiteMatching.RazWigderson.reduction {m e n : ℕ} (p : Communication.KWProtocol (Fin (n * n))) (h : Vertex m e ≃ Fin n) (i₀ : Fin m) (k : ℕ) : Communication.PublicCoin (BitString m) (BitString m) Bool

The Raz–Wigderson reduction: a public-coin protocol for disjointness from a protocol p for the monotone Karchmer–Wigderson game of bipartite perfect matching, running it k times on uniformly random relabellings of the graphs of the reduction.

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.depth_reduction_le {m e n k : ℕ} {p : Communication.KWProtocol (Fin (n * n))} {h : Vertex m e ≃ Fin n} {i₀ : Fin m} : (reduction p h i₀ k).depth ≤ ↑k * (↑(Communication.Protocol.depth p) + 1)

The reduction sends at most k times one more bit than p.

theorem Cslib.Circuits.BipartiteMatching.RazWigderson.solves_reduction {m e n k : ℕ} {p : Communication.KWProtocol (Fin (n * n))} {h : Vertex m e ≃ Fin n} {i₀ : Fin m} (hp : Communication.Protocol.Solves p Communication.ExceedsAt {x : Fin (n * n) → Bool | bipartitePerfectMatching n x = true} {y : Fin (n * n) → Bool | bipartitePerfectMatching n y = false}) (hk : 0 < k) : (reduction p h i₀ k).Solves (1 / 2 ^ k) (fun (x y : BitString m) (b : Bool) => Communication.disjointness x y = b) Set.univ Set.univ

The error of the reduction: it decides disjointness with error at most 2 ^ (-k), for k > 0. On disjoint sets every run answers true; if i₀ is in both sets, every run answers false; otherwise each run answers true with probability at most 1 / 2 (two_mul_card_filter_run_oneRun_le), independently.

theorem Cslib.Circuits.ecomplexityFun_disjointness_le_mul_ecomplexity_bipartitePerfectMatching {m n k : ℕ} (hm : 0 < m) (hmn : 2 * m ≤ n) (hk : 0 < k) : Communication.PublicCoin.ecomplexityFun (1 / 2 ^ k) Communication.disjointness ≤ ↑k * (Communication.Protocol.ecomplexity Communication.ExceedsAt {x : Fin (n * n) → Bool | bipartitePerfectMatching n x = true} {y : Fin (n * n) → Bool | bipartitePerfectMatching n y = false} + 1)

The Raz–Wigderson reduction [RW92]: if the monotone Karchmer–Wigderson game of bipartite perfect matching on K_{n,n} has a protocol sending c bits and 2 m ≤ n with 0 < m, then public-coin protocols decide disjointness of m-bit strings with error 2 ^ (-k) sending at most k (c + 1) bits, for every k > 0.

theorem Cslib.Circuits.le_mul_ecomplexity_bipartitePerfectMatching_add (n : ℕ) : ↑n ≤ 2 ^ 13 * Communication.Protocol.ecomplexity Communication.ExceedsAt {x : Fin (n * n) → Bool | bipartitePerfectMatching n x = true} {y : Fin (n * n) → Bool | bipartitePerfectMatching n y = false} + 2 ^ 14

The monotone Karchmer–Wigderson game of bipartite perfect matching needs Ω(n) bits [RW92]: on K_{n,n}, it needs at least (n - 2 ^ 14) / 2 ^ 13 bits.

theorem Cslib.Circuits.Monotone.le_mul_eformulaDepth_bipartitePerfectMatching_add (n : ℕ) : ↑n ≤ 2 ^ 13 * eformulaDepth (bipartitePerfectMatching n) + 2 ^ 14

Monotone formulas for bipartite perfect matching need linear depth [RW92]: a monotone formula computing whether a subgraph of K_{n,n} has a perfect matching has depth at least (n - 2 ^ 14) / 2 ^ 13, counting AND and OR gates of fan-in two.