Documentation

Complexity.Computability.Circuit.Monotone.Clique.LowerBound

Razborov's lower bound for monotone circuits computing cliques #

Evaluate a monotone circuit computing k-clique in the approximate interpretation. On the complete graphs on k-sets the circuit is right, so the approximator at its output is wrong on at most C(n, k)-many of them only if the circuit is large (Positive.scheme); if it is right on one, it is nonempty. A nonempty approximator accepts at least half of the colourings with k - 1 colours, on which the circuit is right and says false, so it is wrong on half of them, which again needs a large circuit (Negative.scheme). Either way the circuit is large (choose_le_or_pow_le_mul_size), with explicit bounds (lt_size_of_computes_clique) Razborov, Arora and Barak, Theorem 14.7.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Monotone.negativeGateCap (n r p w : ℕ) :
ℕ

The number of negative errors charged to any gate.

Instances For
    source
    noncomputable def Cslib.Circuits.Monotone.outputApproximator {n p w : ℕ} [Fact (2 ≤ p)] (C : Circuit signature (Clique.edgeCount n) 1) :
    Approximator n p w

    The approximator of the output of a circuit.

    Instances For
      source
      theorem Cslib.Circuits.Monotone.nonempty_outputApproximator {n k p w : ℕ} [Fact (2 ≤ p)] (hw : 2 ≤ w) (hk : w + 1 ≤ k) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) (hC' : Positive.errorCap n k p w * C.size < n.choose k) :
      (outputApproximator C).terms.Nonempty

      If the circuit is small, the approximator of its output is right on some complete graph on a k-set, and so is nonempty.

      source
      theorem Cslib.Circuits.Monotone.choose_le_or_pow_le_mul_size {n k p w : ℕ} [Fact (2 ≤ p)] (hw : 2 ≤ w) (hk : w + 1 ≤ k) (hr : 2 * w ^ 2 ≤ k - 1) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) :
      n.choose k ≤ Positive.errorCap n k p w * C.size ∨ (k - 1) ^ n ≤ 2 * negativeGateCap n (k - 1) p w * C.size

      Razborov's dichotomy. A monotone circuit computing k-clique on n vertices exhausts the positive or the negative error budget of the approximators with p petals and width w.

      source
      theorem Cslib.Circuits.Monotone.lt_size_of_computes_clique {n k p w : ℕ} (hp : 2 ≤ p) (hw : 2 ≤ w) (hk : w + 1 ≤ k) (hr : 2 * w ^ 2 ≤ k - 1) {s : ℕ} (hpos : Positive.errorCap n k p w * s < n.choose k) (hneg : 2 * negativeGateCap n (k - 1) p w * s < (k - 1) ^ n) {C : Circuit signature (Clique.edgeCount n) 1} (hC : C.Computes interpretation (single (clique n k))) :
      s < C.size

      Razborov's lower bound. Every monotone circuit computing k-clique on n vertices has more than s gates, for every s below both error budgets of the approximators with p ≥ 2 petals and width w ≥ 2, if w + 1 ≤ k and 2 w ^ 2 ≤ k - 1.