Semifilter bounds for Boolean computations

The true sets of supplied Boolean functions and a designated target output define a semifilter cover problem. Its minimum pair count bounds the AND cost of every native monotone circuit computing the target from those functions. Both raw input variables and positive/negative literals are ordinary source families in this interface; no problem or model wrapper is needed.

Supplied functions are free in ecomplexityFrom. In particular, supplying negative literals does not charge their construction. The circuit itself has only constants, AND and OR gates. Circuits with internal NOT gates are handled in Complexity/Computability/Circuit/Fusion/DeMorgan.lean, through the dual-rail translation, at the cost of a factor two in size.

Main results

• Cslib.Circuits.Fusion.pairCover_lowerBound_of_computesFrom: transfer a combinatorial bound to a concrete circuit computing from supplied Boolean functions.
• Cslib.Circuits.Fusion.pairCoverComplexity_le_ecomplexityFrom_bool: transfer to minimum supplied-source complexity, retaining all designated outputs.

References

• Adapted from LowerBound/Fusion/Boolean.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

theorem Cslib.Circuits.Fusion.pairCover_lowerBound_of_computesFrom {U : Type u_1} {n m : ℕ} (sources : U → Fin n → Bool) (target : U → Fin m → Bool) (o : Fin m) {admissible : Semifilter ↑{x : U | target x o = true}ᶜ → Prop} {k : ℕ} (hbound : ∀ (c : PairCover {x : U | target x o = true} (fun (i : Fin n) => {x : U | sources x i = true}) admissible), k ≤ c.pairs.length) (c : Circuit Monotone.signature n m) (hc : c.ComputesFrom Monotone.interpretation target sources) : k ≤ c.program.cost Monotone.andCost

A lower bound on covers of the true-set problem bounds every Boolean implementation.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_le_ecomplexityFrom_bool {U : Type u_1} {n m : ℕ} (sources : U → Fin n → Bool) (target : U → Fin m → Bool) (o : Fin m) (admissible : Semifilter ↑{x : U | target x o = true}ᶜ → Prop := fun (x : Semifilter ↑{x : U | target x o = true}ᶜ) => True) : pairCoverComplexity {x : U | target x o = true} (fun (i : Fin n) => {x : U | sources x i = true}) admissible ≤ ecomplexityFrom Monotone.interpretation Monotone.andCost target sources

The true-set pair-cover complexity bounds native Boolean source complexity. Sources may be arbitrary supplied functions, including raw variables, helpers and negative literals.