Clique approximators

Razborov's method of approximations for the clique function replaces the value of every gate of a monotone circuit by an approximator: a family of at most sunflowerBound p w sets of at most w vertices, read as the disjunction of the indicators "all edges inside s" (Cslib.Circuits.Monotone.Approximator.decode). An input variable is approximated by its edge, a disjunction by the union of the families, and a conjunction by the pairwise unions of their sets; sets of more than w vertices are dropped, and sunflowers with p petals are plucked (Cslib.pluckNormalForm) to keep the family small. Sets of at most one vertex contain no edges and so stand for true; they are dropped from a pairwise union rather than joined (Cslib.Circuits.Monotone.join).

The approximate interpretation (Cslib.Circuits.Monotone.Approximator.interpretation) makes errors on the two kinds of test inputs, counted in Complexity/Computability/Circuit/Monotone/Clique/Positive.lean and Complexity/Computability/Circuit/Monotone/Clique/Negative.lean.

Main definitions

• Cslib.Circuits.Monotone.Accepts: a family of vertex sets accepts an input.
• Cslib.Circuits.Monotone.Approximator, Cslib.Circuits.Monotone.Approximator.interpretation.

References

• A. A. Razborov, Lower bounds on the monotone complexity of some Boolean functions
• S. Jukna, Boolean Function Complexity: Advances and Frontiers, Chapter 9

def Cslib.Circuits.Monotone.Accepts {n : ℕ} (F : Finset (Finset (Fin n))) (x : Fin (Clique.edgeCount n) → Bool) : Prop

A family of vertex sets accepts an input when the input contains all edges inside one of the sets.

@[instance_reducible]

noncomputable instance Cslib.Circuits.Monotone.instDecidableAccepts {n : ℕ} (F : Finset (Finset (Fin n))) (x : Fin (Clique.edgeCount n) → Bool) : Decidable (Accepts F x)

theorem Cslib.Circuits.Monotone.Accepts.of_forall_exists_subset {n : ℕ} {F G : Finset (Finset (Fin n))} {x : Fin (Clique.edgeCount n) → Bool} (hF : Accepts F x) (h : ∀ s ∈ F, ∃ t ∈ G, t ⊆ s) : Accepts G x

A family accepts whatever a family whose every set contains one of its sets accepts.

theorem Cslib.Circuits.Monotone.contains_of_card_le_one {n : ℕ} (x : Fin (Clique.edgeCount n) → Bool) {s : Finset (Fin n)} (hs : s.card ≤ 1) : Clique.Contains x s

A set of at most one vertex contains no edge.

theorem Cslib.Circuits.Monotone.contains_toFinset_iff {n : ℕ} {x : Fin (Clique.edgeCount n) → Bool} {e : Clique.Edge n} : Clique.Contains x (↑e).toFinset ↔ x ((Clique.edgeEquiv n) e) = true

The input x contains all edges inside the vertices of an edge exactly when it has the edge.

def Cslib.Circuits.Monotone.join {n : ℕ} (s t : Finset (Fin n)) : Finset (Fin n)

The vertex set standing for the conjunction of two sets: a set of at most one vertex stands for true and is dropped.

theorem Cslib.Circuits.Monotone.Contains.of_join {n : ℕ} {x : Fin (Clique.edgeCount n) → Bool} {s t : Finset (Fin n)} (h : Clique.Contains x (join s t)) : Clique.Contains x s ∧ Clique.Contains x t

An input containing all edges inside the join of two sets contains all edges inside each.

theorem Cslib.Circuits.Monotone.contains_join_ofFinset {n : ℕ} {c s t : Finset (Fin n)} (hs : Clique.Contains (Clique.ofFinset c) s) (ht : Clique.Contains (Clique.ofFinset c) t) : Clique.Contains (Clique.ofFinset c) (join s t)

On the complete graph on c, the join of two sets with all edges inside has all edges inside.

def Cslib.Circuits.Monotone.gateTerms {n : ℕ} (w : ℕ) (op : Op) : (Fin (signature.Arity op) → Finset (Finset (Fin n))) → Finset (Finset (Fin n))

The sets produced at a gate from the sets of its arguments, before plucking: {∅} or ∅ for the constants, the union for a disjunction, and the pairwise joins for a conjunction, dropping the sets of more than w vertices.

theorem Cslib.Circuits.Monotone.card_le_of_mem_gateTerms {n w : ℕ} {op : Op} {F : Fin (signature.Arity op) → Finset (Finset (Fin n))} {s : Finset (Fin n)} (hs : s ∈ gateTerms w op F) : s.card ≤ w

structure Cslib.Circuits.Monotone.Approximator (n p w : ℕ) : Type

An approximator: a family of at most sunflowerBound p w sets of at most w vertices.

• terms : Finset (Finset (Fin n))

  The vertex sets.

• card_le_of_mem (s : Finset (Fin n)) : s ∈ self.terms → s.card ≤ w
• card_le : self.terms.card ≤ sunflowerBound p w

noncomputable def Cslib.Circuits.Monotone.Approximator.decode {n p w : ℕ} (A : Approximator n p w) (x : Fin (Clique.edgeCount n) → Bool) : Bool

The truth value of an approximator on an input: whether one of its sets has all edges inside.

@[simp]

theorem Cslib.Circuits.Monotone.Approximator.decode_eq_true {n p w : ℕ} {A : Approximator n p w} {x : Fin (Clique.edgeCount n) → Bool} : A.decode x = true ↔ Accepts A.terms x

noncomputable def Cslib.Circuits.Monotone.Approximator.input {n p w : ℕ} [Fact (2 ≤ p)] (i : Fin (Clique.edgeCount n)) : Approximator n p w

The approximator of an input variable: its edge, if 2 ≤ w.

theorem Cslib.Circuits.Monotone.Approximator.decode_input {n p w : ℕ} [Fact (2 ≤ p)] (hw : 2 ≤ w) (i : Fin (Clique.edgeCount n)) (x : Fin (Clique.edgeCount n) → Bool) : (input i).decode x = x i

noncomputable def Cslib.Circuits.Monotone.Approximator.interpretation {n p w : ℕ} [Fact (2 ≤ p)] : Interpretation signature (Approximator n p w)

The approximate interpretation of the monotone basis: compute the sets at the gate (gateTerms) and pluck sunflowers with p petals.

theorem Cslib.Circuits.Monotone.Approximator.terms_interpretation {n p w : ℕ} [Fact (2 ≤ p)] (op : Op) (A : Fin (signature.Arity op) → Approximator n p w) : (interpretation op A).terms = pluckNormalForm p (gateTerms w op fun (i : Fin (signature.Arity op)) => (A i).terms)