Fusion covers and De Morgan circuit size

The Fusion bounds for Boolean functions are stated for monotone circuits that read positive and negative literals for free, charging only AND gates. This module transfers them to the ordinary size of circuits over the De Morgan basis, where negations may occur anywhere and every gate, constants included, is charged.

Let ρ(f) be the pair-cover complexity of the true set of f from the true sets of its 2 n literals. For the lower bound, the dual-rail translation Monotone.dualRail turns a De Morgan circuit of size s into a monotone circuit of size 2 s on the dual-rail inputs, and these are obtained from the literals by wiring and one free constant. Its AND gates give ρ(f) ≤ 2 s, for any admissible class of semifilters. For the upper bound, the quadratic compiler turns an unrestricted t-pair cover into a monotone circuit with at most 4 (t + 1)² (2 n + t + 1) gates; adding n negations for the literals gives a De Morgan circuit. In the same terms, monotone AND complexity from literals lies between ρ(f) and ρ(f)².

The formalized upper bound is O((t + 1)² (n + t)), cubic in the cover size when t ≥ n rather than quadratic, because unions, free in the AND cost, are charged in size; this is a property of the construction, not a proven lower bound. The formalized size bound depends on n as well as on ρ(f). These formalize known correspondences, not new bounds.

Main definitions

• Cslib.Circuits.Monotone.railSelect: the position of each dual-rail input among the literals.
• Cslib.Circuits.Monotone.literalsRailCircuit: the dual-rail inputs from the literals.

Main results

• Cslib.Circuits.Fusion.ecomplexityFrom_literals_le_pairCoverComplexity_sq, Cslib.Circuits.Fusion.ecomplexityFrom_literals_bounds: ρ(f) ≤ C_∧(f) ≤ ρ(f)² for monotone AND complexity from literals.
• Cslib.Circuits.Fusion.pairCoverComplexity_le_two_mul_size, Cslib.Circuits.Fusion.pairCoverComplexity_le_two_mul_complexity: every De Morgan circuit computing f has at least ρ(f) / 2 gates.
• Cslib.Circuits.Fusion.PairCover.exists_computes_size_le: a t-pair cover gives a De Morgan circuit of size at most 4 (t + 1)² (2 n + t + 1) + n.
• Cslib.Circuits.Fusion.pairCoverComplexity_complexity_bounds: ρ(f) is finite, at most twice De Morgan circuit complexity, which is in turn polynomial in ρ(f) and n.

References

• B. P. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems, Theorem 24, for the quadratic compiler.
• L. M. Goldschlager, The monotone and planar circuit value problems are log space complete for P, for the dual-rail translation.
• Alexander A. Razborov, On the method of approximations, for the method of approximations underlying Fusion.

Dual-rail inputs from literals

def Cslib.Circuits.Monotone.railSelect {n : ℕ} (k : Fin (2 * n + 1)) : Fin (n + n + 1)

Where the dual-rail input k is found among the literals followed by the constant true: input 0 is the constant, input 2 i + 1 the literal x i and input 2 i + 2 its negation.

theorem Cslib.Circuits.Monotone.railBitString_eq_append_literals {n : ℕ} (x : BitString n) (k : Fin (2 * n + 1)) : railBitString x k = Fin.append (Boolean.AltFormula.literals x) (fun (x : Fin 1) => true) (railSelect k)

The dual-rail inputs are a selection from the literals and the constant true.

def Cslib.Circuits.Monotone.literalsRailCircuit (n : ℕ) : Circuit signature (n + n) (2 * n + 1)

A monotone circuit producing the dual-rail inputs from the literals, using a single constant gate and no conjunction.

theorem Cslib.Circuits.Monotone.eval_literalsRailCircuit {n : ℕ} (x : BitString n) : (literalsRailCircuit n).eval interpretation (Boolean.AltFormula.literals x) = railBitString x

@[simp]

theorem Cslib.Circuits.Monotone.cost_literalsRailCircuit {n : ℕ} : (literalsRailCircuit n).program.cost andCost = 0

Monotone AND complexity from literals

theorem Cslib.Circuits.Fusion.PairCover.computesFrom_toCircuit {n : ℕ} {f : BooleanFunction n} (c : PairCover {x : BitString n | f x = true} fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) : c.toCircuit.ComputesFrom Monotone.interpretation (fun (x : BitString n) (x_1 : Fin 1) => f x) Boolean.AltFormula.literals

An unrestricted cover compiles to a monotone circuit computing f from its literals.

theorem Cslib.Circuits.Fusion.ecomplexityFrom_literals_le_pairCoverComplexity_sq {n : ℕ} (f : BooleanFunction n) : ecomplexityFrom Monotone.interpretation Monotone.andCost (fun (x : BitString n) (x_1 : Fin 1) => f x) Boolean.AltFormula.literals ≤ (pairCoverComplexity {x : BitString n | f x = true} fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) ^ 2

Monotone AND complexity from literals is at most the square of unrestricted cover complexity.

theorem Cslib.Circuits.Fusion.ecomplexityFrom_literals_bounds {n : ℕ} (f : BooleanFunction n) : have ρ := pairCoverComplexity {x : BitString n | f x = true} fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}; have C := ecomplexityFrom Monotone.interpretation Monotone.andCost (fun (x : BitString n) (x_1 : Fin 1) => f x) Boolean.AltFormula.literals; ρ ≤ C ∧ C ≤ ρ ^ 2

Monotone AND complexity from literals and cover complexity are polynomially equivalent: the former lies between ρ(f) and ρ(f)², with OR gates and constants free.

De Morgan circuit size

theorem Cslib.Circuits.Fusion.pairCoverComplexity_le_two_mul_size {n : ℕ} {f : BooleanFunction n} (c : Circuit Boolean.signature n 1) (hc : c.Computes Boolean.interpretation (single f)) (admissible : Semifilter ↑{x : BitString n | f x = true}ᶜ → Prop := fun (x : Semifilter ↑{x : BitString n | f x = true}ᶜ) => True) : pairCoverComplexity {x : BitString n | f x = true} (fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) admissible ≤ ↑(2 * c.size)

Fusion lower bound for De Morgan circuits. Every circuit over the De Morgan basis computing f, with negations anywhere, has at least half as many gates as the cover complexity of f from its literals, for any admissible class of semifilters.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_le_two_mul_complexity {n : ℕ} (f : BooleanFunction n) (admissible : Semifilter ↑{x : BitString n | f x = true}ᶜ → Prop := fun (x : Semifilter ↑{x : BitString n | f x = true}ᶜ) => True) : pairCoverComplexity {x : BitString n | f x = true} (fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) admissible ≤ ↑(2 * complexity Boolean.interpretation (single f))

Cover complexity from literals is at most twice De Morgan circuit complexity.

theorem Cslib.Circuits.Fusion.PairCover.exists_computes_size_le {n : ℕ} {f : BooleanFunction n} (c : PairCover {x : BitString n | f x = true} fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) : ∃ (d : Circuit Boolean.signature n 1), d.Computes Boolean.interpretation (single f) ∧ d.size ≤ 4 * ((c.pairs fun (x : Semifilter ↑{x : BitString n | f x = true}ᶜ) => True).length + 1) ^ 2 * (2 * n + (c.pairs fun (x : Semifilter ↑{x : BitString n | f x = true}ᶜ) => True).length + 1) + n

Fusion upper bound for De Morgan circuits. A t-pair cover yields a De Morgan circuit of at most 4 (t + 1)² (2 n + t + 1) + n gates computing f.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_complexity_bounds {n : ℕ} (f : BooleanFunction n) : ∃ (t : ℕ), (pairCoverComplexity {x : BitString n | f x = true} fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) = ↑t ∧ t ≤ 2 * complexity Boolean.interpretation (single f) ∧ complexity Boolean.interpretation (single f) ≤ 4 * (t + 1) ^ 2 * (2 * n + t + 1) + n

Cover complexity and De Morgan circuit size are polynomially related, up to the input length. The cover complexity t = ρ(f) of f from its literals over unrestricted semifilters is finite, at most twice the circuit complexity C(f) over the De Morgan basis, and C(f) ≤ 4 (t + 1)² (2 n + t + 1) + n.