35 Boolean Analysis — Circuit
35.1 Overview
This module sets up the basic combinatorial data of Boolean circuits used in the switching lemma development: literals, general AND/OR circuit trees and their size/depth/fanin measures, normal-form alternating circuits (\(\mathsf{NAnd}\) and \(\mathsf{NOr}\)) with their normalization maps and semantics/size/literal-count preservation results, as well as the auxiliary types (literals, terms, DNF/CNF, and decision trees) needed elsewhere in the switching-lemma proof.
35.2 Declarations
For a literal \(l\) on \(n\) variables and an assignment \(x : \mathrm{Fin}\, n \to \mathbb {F}_2\), the value \(l.\mathrm{eval}\, x\) is \(x_{l.\mathrm{idx}}\) when \(l\) is positive (\(l.\mathrm{sign} = \mathrm{true}\)) and \(\lnot x_{l.\mathrm{idx}}\) when \(l\) is negated.
A Boolean circuit on \(n\) variables is a tree whose leaves are literals (lit \(l\)) and whose internal nodes (node \(isAnd\) \(children\)) are AND gates when \(isAnd = \mathrm{true}\) and OR gates when \(isAnd = \mathrm{false}\), applied to a list of child circuits. No alternation or deduplication constraint is imposed.
Let \(P\) be a property of Boolean circuits on \(n\) variables. Suppose that \(P\) holds for every literal circuit, and that whenever \(P\) holds for every circuit in a list \(cs\) of children, it also holds for the gate circuit \(\mathrm{node}(isAnd, cs)\) formed from \(cs\) (an AND gate when \(isAnd = \mathrm{true}\), an OR gate when \(isAnd = \mathrm{false}\)). Then \(P\) holds for every Boolean circuit on \(n\) variables.
Evaluates a circuit under an assignment \(x\): a literal evaluates via \(\mathrm{Lit.eval}\), an AND node is the conjunction (foldr with &&, unit true) of its children’s values, and an OR node is the disjunction (foldr with ||, unit false).
The number of literal occurrences in a circuit: a literal contributes \(1\) and a node contributes the sum of the literal counts of its children.
The depth of a circuit (longest root-to-leaf path): a literal has depth \(0\) and a node has depth \(1\) plus the maximum depth among its children.
The total number of nodes of a circuit (internal gates plus literal leaves): a literal has size \(1\) and a node has size \(1\) plus the sum of the sizes of its children.
The maximum depth over a list \(cs\) of circuits (with \(0\) for the empty list), used to compute the depth at a node.
The sum of the sizes over a list \(cs\) of circuits, used to compute the size at a node.
The maximum fanin of a circuit: a literal has fanin \(0\), and a node’s value is the maximum of the number of its children and the maximal fanin occurring recursively among its children.
A normal-form AND circuit on \(n\) variables: either a base clause given by a list of literals whose variable indices are pairwise distinct (a Nodup proof on \(lits.\mathrm{map}\; \mathrm{Lit.idx}\)), or a node that ANDs together a list of normal-form OR circuits. Together with \(\mathrm{NOrCircuit}\) this forms a strictly alternating AND/OR normal form.
Evaluates a normal-form AND circuit under an assignment \(x\): a clause is the conjunction of its literals’ values (unit true), and a node is the conjunction of its child OR circuits’ values.
Evaluates a normal-form OR circuit under an assignment \(x\): a clause is the disjunction of its literals’ values (unit false), and a node is the disjunction of its child AND circuits’ values.
The number of literal occurrences in a normal-form AND circuit: a clause contributes the length of its literal list, and a node contributes the sum over its child OR circuits.
The number of literal occurrences in a normal-form OR circuit: a clause contributes the length of its literal list, and a node contributes the sum over its child AND circuits.
The total node count of a normal-form AND circuit: a clause has size \(1\), and a node has size \(1\) plus the sum of the sizes of its child OR circuits.
The total node count of a normal-form OR circuit: a clause has size \(1\), and a node has size \(1\) plus the sum of the sizes of its child AND circuits.
The depth of a normal-form AND circuit: a clause has depth \(0\), and a node has depth \(1\) plus the maximum depth among its child OR circuits.
The depth of a normal-form OR circuit: a clause has depth \(0\), and a node has depth \(1\) plus the maximum depth among its child AND circuits.
Fix \(n\), and let \(lits\) be a list of literals over the variables \(\{ 0,\dots ,n-1\} \) whose underlying variable indices, obtained by taking the index of each literal in \(lits\), are pairwise distinct. If a normal-form AND circuit on \(n\) variables equals the base clause built from \(lits\) together with this distinctness witness, then the list of variable indices of \(lits\) has no repeated entries.
Fix a natural number \(n\), and let \(\ell \) be a list of literals over \(n\) variables, each literal being a pair consisting of a variable index in \(\mathrm{Fin}\, n\) and a sign in \(\mathrm{Bool}\). Suppose the variable indices occurring in \(\ell \) are pairwise distinct, and let \(c\) be the OR-clause circuit built from \(\ell \) under this distinctness hypothesis. Then the list of variable indices of \(\ell \) is duplicate-free, i.e. its entries are pairwise distinct.
Let \(\ell _1,\dots ,\ell _m\) be a list of circuit literals over \(n\) variables whose variable indices are pairwise distinct. Then any two literals \(l_1\) and \(l_2\) in this list that have the same variable index are equal; that is, if \(l_1\) and \(l_2\) both occur in the list and \(l_1.\mathrm{idx} = l_2.\mathrm{idx}\), then \(l_1 = l_2\).
Converts a general circuit into a normal-form AND circuit: a literal becomes a singleton clause; an AND node maps its children through \(\mathrm{toNOr}\); and an OR node is wrapped as a single OR node built from the children’s \(\mathrm{toNAnd}\) images, enforcing alternation.
Converts a general circuit into a normal-form OR circuit: a literal becomes a singleton clause; an OR node maps its children through \(\mathrm{toNAnd}\); and an AND node is wrapped as a single AND node built from the children’s \(\mathrm{toNOr}\) images, enforcing alternation.
Let \(\alpha \) and \(\beta \) be types, let \(f\colon \alpha \to \{ \mathrm{true},\mathrm{false}\} \) and \(g\colon \beta \to \{ \mathrm{true},\mathrm{false}\} \) be Boolean-valued functions, let \(h\colon \alpha \to \beta \), and let \(cs\) be a finite list of elements of \(\alpha \). Suppose that \(g(h(c)) = f(c)\) for every \(c\) appearing in \(cs\). Then the Boolean conjunction of \(g\) over the mapped list, \(\bigwedge _{c\in cs} g(h(c))\), equals the Boolean conjunction of \(f\) over \(cs\), namely \(\bigwedge _{c\in cs} f(c)\), where in each case the conjunction is folded from the right starting from \(\mathrm{true}\).
Let \(f : \alpha \to \{ \text{true},\text{false}\} \) and \(g : \beta \to \{ \text{true},\text{false}\} \) be Boolean-valued functions, let \(h : \alpha \to \beta \), and let \(c_1, \dots , c_n\) be a finite list of elements of \(\alpha \). If \(g(h(c)) = f(c)\) for every element \(c\) of the list, then the disjunction \(g(h(c_1)) \vee \cdots \vee g(h(c_n))\) of the values of \(g\) over the mapped list equals the disjunction \(f(c_1) \vee \cdots \vee f(c_n)\) of the values of \(f\) over the original list, where each empty disjunction is taken to be \(\text{false}\).
Let \(f\colon A \to \mathbb {N}\) and \(g\colon B \to \mathbb {N}\) be functions into the natural numbers, let \(h\colon A \to B\) be a map, and let \(c_1,\dots ,c_m\) be a finite list of elements of \(A\). If \(g(h(c)) = f(c)\) for every entry \(c\) of the list, then
where each sum is taken over the list in order with initial value \(0\).
Let \(f\colon \alpha \to \mathbb {N}\), \(g\colon \beta \to \mathbb {N}\), and \(h\colon \alpha \to \beta \) be functions into the natural numbers, let \(cs\) be a finite list of elements of \(\alpha \), and let \(k\in \mathbb {N}\). If \(g(h(c)) \le k\, f(c)\) holds for every entry \(c\) of \(cs\), then, summing over the entries of \(cs\) (with multiplicity),
Let \(c\) be a Boolean circuit on \(n\) variables and let \(x : \mathrm{Fin}\, n \to \mathbb {F}_2\) be an assignment. Then both alternating normal forms of \(c\) compute the same value as \(c\) itself: the normal-form AND circuit obtained by normalizing \(c\) evaluates at \(x\) to \(c\)’s value, and likewise the normal-form OR circuit obtained by normalizing \(c\) evaluates at \(x\) to \(c\)’s value.
Let \(c\) be a Boolean circuit on \(n\) variables — a tree of literals combined by AND and OR gates — and let \(x : \mathrm{Fin}\, n \to \mathbb {F}_2\) be an assignment to those variables. Converting \(c\) into strictly alternating AND-normal form and evaluating the resulting normal-form AND circuit at \(x\) yields the same Boolean value as evaluating \(c\) directly at \(x\).
Let \(c\) be a Boolean circuit on \(n\) variables and let \(x : \mathrm{Fin}\, n \to \mathbb {F}_2\) be an assignment. Then the normal-form OR circuit obtained by OR-normalizing \(c\) computes the same Boolean value as \(c\) itself: evaluated at \(x\), it agrees with the value of \(c\) at \(x\).
Let \(c\) be a Boolean circuit on \(n\) variables, whose literal count is the number of literal occurrences it contains (a leaf literal counting once, and an AND or OR gate counting the total over its children). Converting \(c\) to strictly alternating AND/OR normal form preserves this count: both the AND-normal form of \(c\) and the OR-normal form of \(c\) have the same number of literal occurrences as \(c\) itself.
Let \(c\) be a Boolean circuit on \(n\) variables, and let \(c'\) be the normal-form AND circuit obtained by normalizing it (a literal becomes a singleton clause, an AND gate normalizes each child to OR-normal form, and an OR gate is wrapped as a single OR node over the AND-normalizations of its children). Then \(c'\) contains exactly as many literal occurrences as \(c\): the number of literals in \(c'\) equals the number of literals in \(c\).
For every Boolean circuit \(c\) on \(n\) variables, converting \(c\) to OR-normal form leaves its total number of literal occurrences unchanged: the literal count of the normal-form OR circuit obtained from \(c\) equals the literal count of \(c\) itself.
Let \(c\) be a Boolean circuit on \(n\) variables, and write \(\mathrm{size}(c)\) for its total node count. Converting \(c\) into either alternating normal form increases its size by at most a factor of two: the normal-form AND circuit obtained by normalizing \(c\) has size at most \(2\, \mathrm{size}(c)\), and the normal-form OR circuit obtained by normalizing \(c\) likewise has size at most \(2\, \mathrm{size}(c)\).
Let \(c\) be a Boolean circuit on \(n\) variables, where the size of a circuit is its total number of nodes, counting internal AND/OR gates together with literal leaves. Normalizing \(c\) into strictly alternating AND-normal form — a literal becoming a singleton clause, an AND gate normalizing each child into OR-normal form, and an OR gate becoming a single wrapping OR node over its children’s AND-normal forms — yields a normal-form AND circuit whose size is at most twice the size of \(c\).
Let \(c\) be a Boolean circuit on \(n\) variables, and let \(\mathrm{size}(c)\) denote its total node count (literal leaves plus internal AND/OR gates). Write \(c'\) for the OR-normal form of \(c\), the normal-form OR circuit obtained by rewriting \(c\) into strictly alternating AND/OR normal form. Then the size of \(c'\) is at most twice the size of \(c\):
The forgetful map turning a normal-form AND circuit into a general circuit: a clause becomes an AND node over its literals, and a node becomes an AND node over the circuit images of its child OR circuits.
The forgetful map turning a normal-form OR circuit into a general circuit: a clause becomes an OR node over its literals, and a node becomes an OR node over the circuit images of its child AND circuits.
The normal-form AND circuit consisting of the single positive literal on variable \(i\).
The normal-form OR circuit consisting of the single positive literal on variable \(i\).
The constant-true AND circuit, given by the empty clause (an empty conjunction).
The constant-false OR circuit, given by the empty clause (an empty disjunction).
For a literal \(l\) with variable \(l.\mathrm{var}\) and polarity \(l.\mathrm{neg}\) and an assignment \(x\), the value is \(x_{l.\mathrm{var}}\) for a positive literal and \(\lnot x_{l.\mathrm{var}}\) for a negated one.
The width of a CNF formula \(c\), defined as the maximum width over its clauses (and \(0\) for the empty formula).
Evaluates a decision tree on an input \(x\): a leaf returns its stored bit, and a branch on variable \(i\) follows the high subtree when \(x_i\) is true and the low subtree otherwise.
The depth of a decision tree (maximum path length to a leaf): a leaf has depth \(0\) and a branch has depth \(1\) plus the maximum of its two subtrees’ depths.
Extracts a deepest root-to-leaf path from a decision tree, at each branch descending into the deeper subtree (ties broken toward the high subtree). It returns the list of \((\text{queried variable}, \text{branch direction})\) pairs along that path.
Let \(T\) be a decision tree on \(n\) Boolean variables. Then the deepest root-to-leaf path of \(T\) has length equal to the depth of \(T\); that is, the number of branch queries along that path is exactly \(\mathrm{depth}(T)\).
Let \(f\colon \{ 0,1\} ^n \to \{ 0,1\} \) be a Boolean function on \(n\) variables, let \(k \le n\), and let \(acc\) be a partial assignment of the variables. Then the full decision tree for \(f\) that queries the variables \(k, k+1, \dots , n-1\) in order starting from \(acc\) has depth at most \(n - k\).
Let \(f \colon (\mathbb {F}_2)^n \to \{ \mathtt{true},\mathtt{false}\} \) be a Boolean function on \(n\) variables, let \(k \le n\), and let \(acc, x \colon \{ 0,\dots ,n-1\} \to \{ \mathtt{true},\mathtt{false}\} \) be two assignments that agree on every coordinate below \(k\), that is \(acc_i = x_i\) for all \(i \lt k\). Then the full decision tree for \(f\) that branches on variables \(k, k+1, \dots , n-1\) starting from the accumulator \(acc\) evaluates on input \(x\) to \(f(x)\).
35.3 Base literal, formula, and decision-tree definitions
A literal for Boolean circuits: a variable index \(\mathtt{idx} : \mathrm{Fin}\, n\) together with a polarity \(\mathtt{sign} : \mathrm{Bool}\) (true = positive occurrence).
A literal for switching-lemma formulas: a variable \(\mathtt{var} : \mathrm{Fin}\, n\) with a negation flag \(\mathtt{neg} : \mathrm{Bool}\) (true = negated literal).
A term is a conjunction of literals, represented as a list: \(\mathtt{Term}\, n = \mathtt{List}\, (\mathtt{Literal}\, n)\).
The width of a term is its number of literals (the list length).
A term evaluates to true on input \(x\) iff every literal in it holds under \(x\) (conjunction semantics).
A DNF formula is a disjunction of terms, represented as a list: \(\mathtt{DNF}\, n = \mathtt{List}\, (\mathtt{Term}\, n)\).
The width of a DNF formula is the maximum width of its terms (\(0\) for the empty formula).
A DNF formula evaluates to true on input \(x\) iff at least one of its terms holds under \(x\) (disjunction of conjunctions).
A CNF formula is a conjunction of clauses, each clause a disjunction of literals; it is represented as \(\mathtt{CNF}\, n = \mathtt{List}\, (\mathtt{Term}\, n)\) with dual evaluation semantics.
A single CNF clause evaluates to true on input \(x\) iff some literal in it holds under \(x\) (disjunction semantics).
A CNF formula evaluates to true on input \(x\) iff every clause holds under \(x\).
A decision tree on \(n\) Boolean variables: a leaf \(\mathtt{leaf}\, b\) outputs \(b\), and a branch \(\mathtt{branch}\, i\, lo\, hi\) queries variable \(i\), following \(lo\) on false and \(hi\) on true.
The complete decision tree for a function \(f\) that queries variables \(k, k+1, \dots , n-1\) in order, starting from accumulator assignment \(acc\), and outputs \(f\) applied to the completed assignment at each leaf.
The decision-tree depth of \(f : (\mathrm{Fin}\, n \to \mathrm{Bool}) \to \mathrm{Bool}\) is the least \(d\) such that some decision tree of depth at most \(d\) computes \(f\); it is well defined since the full tree computes \(f\) at depth \(n\).