Counting accepted and satisfying inputs of Boolean circuits

Defines exact acceptance and satisfying-input counts (Circuit.acceptCount, Circuit.satCount) for circuits interpreted over Bool under an arbitrary signature σ.

Main definitions

• Cslib.Circuits.Circuit.acceptCount: number of inputs x : Fin n → Bool on which every output o satisfies acc o.
• Cslib.Circuits.Circuit.satCount: number of satisfying inputs x : Fin n → Bool of a single-output Boolean circuit (c.eval I x 0 = true).

Main results

• Cslib.Circuits.Circuit.satCount_eq_acceptCount: satCount is acceptCount accepting true at output 0.
• Cslib.Circuits.Circuit.acceptCount_eq_ncard: acceptCount agrees with Set.ncard of the accepted input set.
• Cslib.Circuits.Circuit.satCount_pos_iff: satCount is positive if and only if the circuit has a satisfying input.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

def Cslib.Circuits.Circuit.acceptCount {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ Bool) (acc : Fin m → Bool → Bool) : ℕ

Number of inputs x : Fin n → Bool on which every output o satisfies acc o.

def Cslib.Circuits.Circuit.satCount {σ : Signature} {n : ℕ} (c : Circuit σ n 1) (I : Interpretation σ Bool) : ℕ

Number of satisfying inputs x : Fin n → Bool of a single-output Boolean circuit (c.eval I x 0 = true).

theorem Cslib.Circuits.Circuit.satCount_eq_acceptCount {σ : Signature} {n : ℕ} (c : Circuit σ n 1) (I : Interpretation σ Bool) : c.satCount I = c.acceptCount I fun (x : Fin 1) (b : Bool) => b

Single-output satCount is acceptCount accepting true at output 0.

theorem Cslib.Circuits.Circuit.acceptCount_eq_ncard {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ Bool) (acc : Fin m → Bool → Bool) : c.acceptCount I acc = {x : Fin n → Bool | ∀ (o : Fin m), acc o (c.eval I x o) = true}.ncard

acceptCount agrees with Set.ncard of the accepted input set.

theorem Cslib.Circuits.Circuit.satCount_pos_iff {σ : Signature} {n : ℕ} (c : Circuit σ n 1) (I : Interpretation σ Bool) : 0 < c.satCount I ↔ ∃ (x : Fin n → Bool), c.eval I x 0 = true

satCount is positive iff the circuit has a satisfying input.