Sparse truth-table synthesis

Each row is divided into short tuples of true columns. All possible tuples are implemented once. The leading assembly cost is weight / chunkSize.

def Complexity.CircuitSparseSynthesis.Internal.sparseTableBudget (k l K weight : ℕ) : ℕ

Shared minterms, all K-tuples of columns, and one OR per selected sparse chunk.

Equations

• Complexity.CircuitSparseSynthesis.Internal.sparseTableBudget k l K weight = (2 ^ k + 2 ^ l) * (2 * (k + l) + 1) + (2 ^ k + 1) ^ K * (K + 1) + weight / K + 4 * 2 ^ l + 1

theorem Complexity.CircuitSparseSynthesis.Internal.sparseTable_synthesis {k l : ℕ} (domain : Finset (Fin (k + l) → Bool)) (K : ℕ) (positive : 0 < K) : Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.inputs (k + l)) {fun (x : Fin (k + l) → Bool) => decide (x ∈ domain)} (sparseTableBudget k l K domain.card)

theorem Complexity.CircuitSparseSynthesis.Internal.exists_sparseTable {k l : ℕ} (domain : Finset (Fin (k + l) → Bool)) (K : ℕ) (positive : 0 < K) : ∃ (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature (k + l) 1), (c.Computes Cslib.Circuits.Boolean.interpretation fun (x : Fin (k + l) → Bool) (x_1 : Fin 1) => decide (x ∈ domain)) ∧ c.size ≤ sparseTableBudget k l K domain.card