Sparse and partial synthesis: the constructions

This file builds De Morgan circuits, with explicit gate budgets, for two kinds of Boolean functions that carry little information: the indicator of a small set of inputs (complexity_indicator_le_indicatorBound), and a function that only has to be correct on a small set of inputs (complexityOn_le_partialBound). The file Complexity.Computability.Circuit.Boolean.SparseSynthesis chooses the parameters and shows that, for sets of 2 ^ p of the 2 ^ (2 p) inputs, the budgets are (1 + o(1)) 2 ^ p and (1 + o(1)) 2 ^ p / p. No asymptotics happen here. The constructions follow Chashkin's account Chashkin, Sections 2 and 3 of the methods of Lupanov [Lup65], Nechiporuk [Nec65], Sholomov [Sho69] and Andreev [And89].

Tables

Split k + l input bits into k column bits and l row bits, and view a truth table as a matrix with 2 ^ l rows and 2 ^ k columns. Every column minterm and every row minterm is built once. Each row is a disjunction of patterns, sets of columns that are built once from the column minterms and shared by all rows, so beyond a fixed overhead a table costs one gate per pattern chosen in a row.

• A sparse table computes the indicator of a set D: the true entries of each row are cut into chunks of K, and every set of at most K columns is a pattern. About |D| / K patterns are chosen.
• A partial table computes a function given on a set D: the given entries of each row are cut into chunks of J consecutive entries. On a chunk, the function agrees with some assignment to all columns from a bank of (2 · 2 ^ k + 1) 2 ^ J assignments, chosen by a covering bound, which extends every assignment to at most J columns Chashkin, Lemma 2.1. Masked to the interval of columns spanned by the chunk, that assignment is a pattern and does not interfere with the other chunks Chashkin, Lemma 2.2. About |D| / J patterns are chosen.

Hashing

A table only has few patterns when it has few columns, so the inputs are first hashed to k + l bits by a linear map over the field with two elements. Two distinct inputs collide under a 2 ^ -(k + l) fraction of the linear maps, so some linear map makes at most that fraction of any given pairs of distinct inputs collide Chashkin, Lemmas 2.3 and 2.4.

• For a function given on D, tabulate it on the image of D under one hash, and correct, by explicit minterms, the few inputs of D whose hash collides with that of another input of D.
• For the indicator of a set B with |B| ≤ 2 ^ p, a hash to k + l = p + a bits followed by a sparse table for the image of B is a filter: true on B, and on at most a 2 ^ -a fraction of the other inputs. The conjunction of t filters wrongly accepts at most 2 ^ n / 2 ^ (a t) inputs, which are removed by explicit minterms Chashkin, Lemma 3.3.

The collision bound uses the shared BitString.LinearHash API; the circuit implementation uses finite-set parity masks to retain its exact gate bound.

Main definitions

• Cslib.Circuits.Boolean.SparseSynthesis.sparseTableBound, Cslib.Circuits.Boolean.SparseSynthesis.partialTableBound: the budgets of the tables.
• Cslib.Circuits.Boolean.SparseSynthesis.indicatorBound: the budget for sparse indicators.
• Cslib.Circuits.Boolean.SparseSynthesis.partialBound: the budget for partial functions.

Main results

• Cslib.Circuits.Boolean.SparseSynthesis.complexity_indicator_le_indicatorBound: the indicator of a set of at most 2 ^ p inputs costs at most indicatorBound n k l K p a t gates.
• Cslib.Circuits.Boolean.SparseSynthesis.complexityOn_le_partialBound: a function on a set D of inputs costs at most partialBound n k l J |D| gates on D.

References

• A. V. Chashkin, On computing partial Boolean functions
• O. B. Lupanov, On an approach to the synthesis of control systems: the principle of local coding
• E. I. Nechiporuk, On the complexity of gating circuits realizing Boolean matrices with undefined elements
• L. A. Sholomov, On the realization of incompletely defined Boolean functions by circuits of functional elements
• A. E. Andreev, On the complexity of the realization of partial Boolean functions by circuits of functional elements

Tables with shared column patterns

Blocks of consecutive elements

Sparse tables

def Cslib.Circuits.Boolean.SparseSynthesis.sparseTableBound (k l K w : ℕ) : ℕ

The gate budget of a sparse table on k + l inputs with w true entries and chunks of K columns: the shared minterms of the 2 ^ k columns and the 2 ^ l rows, every one of the (2 ^ k + 1) ^ K patterns of at most K columns, one gate per chunk, about w / K of them, and four gates per row.

Banks of extensions

Partial tables

def Cslib.Circuits.Boolean.SparseSynthesis.partialTableBound (k l J w : ℕ) : ℕ

The gate budget of a partial table on k + l inputs with w specified entries and chunks of J specified entries: the shared minterms of the columns and the rows, the at most (2 ^ k + 1) ^ 2 (2 · 2 ^ k + 1) 2 ^ J patterns given by an interval of columns and an assignment from a bank of extensions, each of at most 2 ^ k columns, one gate per chunk, about w / J of them, and four gates per row.

Linear hashing

Sparse indicators

def Cslib.Circuits.Boolean.SparseSynthesis.indicatorBound (n k l K p a t : ℕ) : ℕ

The gate budget of the construction for the indicator of a set of at most 2 ^ p of the 2 ^ n inputs: t filters, each hashing to k + l = p + a bits and looking the hash up in a sparse table with chunks of K columns, and explicit minterms for the at most 2 ^ n / 2 ^ (a t) inputs that wrongly pass every filter.

theorem Cslib.Circuits.Boolean.SparseSynthesis.complexity_indicator_le_indicatorBound {n p a k l K : ℕ} (B : Finset (BitString n)) (hB : B.card ≤ 2 ^ p) (hkl : k + l = p + a) (hK : 0 < K) (t : ℕ) : complexity interpretation (single fun (x : Fin n → Bool) => decide (x ∈ B)) ≤ indicatorBound n k l K p a t

Sparse indicators. The indicator of a set of at most 2 ^ p inputs costs at most indicatorBound n k l K p a t gates, whenever k + l = p + a and K > 0.

Partial functions

def Cslib.Circuits.Boolean.SparseSynthesis.partialBound (n k l J w : ℕ) : ℕ

The gate budget of the construction for a function on a set of w of the 2 ^ n inputs: a hash to k + l bits, a partial table with chunks of J entries for the values on the image, and explicit minterms correcting the at most w ^ 2 / 2 ^ (k + l) inputs whose hashes collide with others.

theorem Cslib.Circuits.Boolean.SparseSynthesis.complexityOn_le_partialBound {n : ℕ} (k l : ℕ) {J : ℕ} (D : Finset (BitString n)) (u : BooleanFunction n) (hJ : 0 < J) : complexityOn interpretation (↑D) (single u) ≤ partialBound n k l J D.card

Partial functions. A Boolean function on a set D of inputs costs at most partialBound n k l J |D| gates on D, whenever J > 0.