Monotone circuit lower bound for clique

DefinitionThe clique function on adjacency-matrix bits#✓fully proved

For a natural number \(n\) and a bitstring \(x\), read \(x\) as an \(n \times n\) adjacency matrix in row-major order: the entry for a pair \((a, b)\) is the bit of \(x\) at position \(an + b\), where a position beyond the end of \(x\) reads as false. The clique predicate holds for \(n\) and \(x\) when there is a set \(S\) of exactly \(\lfloor n/3 \rfloor\) vertices among \(0, \dots, n - 1\) such that the entry for \((a, b)\) is true for all distinct \(a, b \in S\).

def cliqueHolds (n : ℕ) (x : List Bool) : Prop :=
  ∃ S : Finset ℕ, S.card = n / 3 ∧ (∀ v ∈ S, v < n) ∧
    ∀ a ∈ S, ∀ b ∈ S, a ≠ b → x.getD (a * n + b) false = true

Used by 1

Used byRazborov: monotone circuits for clique need superpolynomial size

TheoremRazborov: monotone circuits for clique need superpolynomial size#●ready to prove

For every polynomial \(p\) with natural-number coefficients there is a natural number \(n\) with the following property. Let \(C\) be a well-formed monotone flat circuit on \(n^2\) inputs, that is, every gate of \(C\) is an input variable, an and gate or an or gate, and refers only to earlier gates. Suppose that for every bitstring \(x\) of length \(n^2\), when input variable \(i\) is given the \(i\)-th bit of \(x\), \(C\) has a last gate with value true if and only if the \(n \times n\) matrix read from \(x\) in row-major order has a clique of size \(\lfloor n/3 \rfloor\), that is, a set \(S \subseteq \{0, \dots, n - 1\}\) of \(\lfloor n/3 \rfloor\) vertices whose entries \((a, b)\) are true for all distinct \(a, b \in S\). Then \(C\) has more than \(p(n^2)\) gates.

public theorem_wanted razborov_monotone_clique :
    ∀ p : Polynomial ℕ, ∃ n : ℕ, ∀ C : List (ACGate (n * n)),
      WellFormedCircuit C → IsMonotoneCircuit C →
        (∀ x : List Bool, x.length = n * n →
          ((circuitEval C (fun i => x.getD (i : ℕ) false)).getLast? = some true ↔
            cliqueHolds n x)) →
          C.length > p.eval (n * n)

inductive ACGate (n : ℕ) where
  | var : Fin n → ACGate n
  | const : Bool → ACGate n
  | notGate : ℕ → ACGate n
  | andGate : List ℕ → ACGate n
  | orGate : List ℕ → ACGate n
  | modGate : ℕ → List ℕ → ACGate n

CSLibExt/Computability/Complexity/Classes.lean:414

def WellFormedCircuit {n : ℕ} (C : List (ACGate n)) : Prop :=
  ∀ j (h : j < C.length), ∀ a ∈ gateInputs (C[j]'h), a < j

CSLibExt/Computability/Complexity/Classes.lean:432

def IsMonotoneCircuit {n : ℕ} (C : List (ACGate n)) : Prop :=
  ∀ g ∈ C, match g with
    | .var _ => True
    | .andGate _ => True
    | .orGate _ => True
    | _ => False

CSLibExt/Computability/Complexity/Classes.lean:550

def circuitEval {n : ℕ} (C : List (ACGate n)) (assign : Fin n → Bool) : List Bool :=
  C.foldl (fun vs g => vs ++ [gateValue vs assign g]) []

CSLibExt/Computability/Complexity/Classes.lean:447

def cliqueHolds (n : ℕ) (x : List Bool) : Prop :=
  ∃ S : Finset ℕ, S.card = n / 3 ∧ (∀ v ∈ S, v < n) ∧
    ∀ a ∈ S, ∀ b ∈ S, a ≠ b → x.getD (a * n + b) false = true

WantedExt/Complexity/KeyTheorems/RazborovMonotoneCliqueWanted.lean:43

Sources

A. A. Razborov, "Lower bounds on the monotone complexity of some Boolean functions", Soviet Mathematics Doklady 31 (1985), 354-357.

Uses 5

Statement usesGates of a flat Boolean circuit · Monotone circuits · Well-formed flat circuits · Evaluation of a flat Boolean circuit · The clique function on adjacency-matrix bits

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.