22 Boolean Analysis — Circuit Helpers
22.1 Overview
This module collects helper lemmas and constructions used to prove switching-lemma bounds for depth-\(2\) Boolean circuits in the LMN development. It provides a cleaning procedure that removes contradictory and duplicated literals from DNF/CNF formulas (while preserving their evaluation and not increasing width), general switching-lemma bounds that drop the syntactic “no duplicate variable” requirement, and translations from shallow Boolean circuits into DNF/CNF formulas.
22.2 Declarations
If \(f,g:(\mathrm{Fin}\, n\to \{ 0,1\} )\to \{ 0,1\} \) agree pointwise, i.e. \(f(x)=g(x)\) for all \(x\), then for every restriction \(\rho \) the restricted functions coincide: \(\mathrm{restrictFn}\, f\, \rho = \mathrm{restrictFn}\, g\, \rho \).
If \(f\) and \(g\) agree pointwise, then for any \(p\in \mathbb {R}\) and \(t\in \mathbb {N}\) the Bernoulli restriction probabilities of the events \(\{ \rho : \mathrm{dtDepth}(\mathrm{restrictFn}\, f\, \rho ) \gt t\} \) and \(\{ \rho : \mathrm{dtDepth}(\mathrm{restrictFn}\, g\, \rho ) \gt t\} \) are equal.
Given a term \(t\) (a list of literals), \(\mathrm{dedupTermVar}\, t\) keeps each literal only if no earlier-retained literal already uses the same variable, removing literals whose variable already appeared.
\(\mathrm{termHasContradiction}\, t\) returns true iff the term \(t\) contains two literals on the same variable with opposite polarities (one negated, one not).
\(\mathrm{cleanDNF}\, d\) first discards every contradictory term of the DNF \(d\) and then applies \(\mathrm{dedupTermVar}\) to each remaining term.
\(\mathrm{cleanCNF}\, c\) filters out the contradictory (tautological) clauses of the CNF \(c\) and then de-duplicates the literals of each remaining clause via \(\mathrm{dedupTermVar}\).
For every term \(t\), the de-duplicated term \(\mathrm{dedupTermVar}\, t\) has no repeated literals (it satisfies Nodup).
Within \(\mathrm{dedupTermVar}\, t\) the variable of a literal determines the literal: any two literals \(l_1,l_2\in \mathrm{dedupTermVar}\, t\) with \(l_1.\mathrm{var}=l_2.\mathrm{var}\) are equal.
The de-duplicated term is no longer than the original: \((\mathrm{dedupTermVar}\, t).\mathrm{length} \le t.\mathrm{length}\).
If \(\mathrm{termHasContradiction}\, t = \texttt{true}\), then for every input \(x\) the term evaluates to false under conjunction: \(\mathrm{Term.eval}\, t\, x = \texttt{false}\).
For a non-contradictory term \(t\) (i.e. \(\mathrm{termHasContradiction}\, t = \texttt{false}\)), de-duplication does not change the conjunction value: \(\mathrm{Term.eval}\, (\mathrm{dedupTermVar}\, t)\, x = \mathrm{Term.eval}\, t\, x\) for all \(x\).
For every DNF \(d\) and input \(x\), the cleaned formula computes the same Boolean function: \((\mathrm{cleanDNF}\, d).\mathrm{eval}\, x = d.\mathrm{eval}\, x\).
If \(\mathrm{termHasContradiction}\, t = \texttt{true}\), then viewed as a clause \(t\) is a tautology: \(\mathrm{CNF.evalClause}\, t\, x = \texttt{true}\) for every \(x\).
For a non-contradictory clause \(t\), de-duplication preserves the disjunctive (clause) value: \(\mathrm{CNF.evalClause}\, (\mathrm{dedupTermVar}\, t)\, x = \mathrm{CNF.evalClause}\, t\, x\).
For every CNF \(c\) and input \(x\), cleaning preserves the computed function: \(\mathrm{CNF.eval}\, (\mathrm{cleanCNF}\, c)\, x = \mathrm{CNF.eval}\, c\, x\).
The cleaned DNF has width at most that of the original: \((\mathrm{cleanDNF}\, d).\mathrm{width} \le d.\mathrm{width}\).
The cleaned CNF has width at most that of the original: \(\mathrm{CNF.width}\, (\mathrm{cleanCNF}\, c) \le \mathrm{CNF.width}\, c\).
In every term of \(\mathrm{cleanDNF}\, d\), the variable determines the literal: for each such term, any two of its literals with the same variable are equal.
Every term of \(\mathrm{cleanDNF}\, d\) satisfies Nodup, i.e. contains no repeated literal.
In every clause of \(\mathrm{cleanCNF}\, c\), the variable determines the literal: any two literals of the clause sharing a variable are equal.
Every clause of \(\mathrm{cleanCNF}\, c\) satisfies Nodup.
Let \(f\) be a DNF of width at most \(w\) with \(0\lt w\) and \(0\lt n\), and let \(p\in \mathbb {R}\) satisfy \(0\lt p\), \(p\le \tfrac {1}{40w}\) and \(p\le 1\). Then for every \(t\in \mathbb {N}\),
Unlike the base version, no syntactic non-duplication hypothesis is required, since the formula is first cleaned.
Let \(f\) be a CNF of width at most \(w\) with \(0\lt w\) and \(0\lt n\), and let \(p\in \mathbb {R}\) satisfy \(0\lt p\), \(p\le \tfrac {1}{40w}\) and \(p\le 1\). Then for every \(t\in \mathbb {N}\),
again without any non-duplication hypothesis on \(f\).
If a gate node \(\mathrm{node}\, \mathit{isAnd}\, cs\) has depth at most \(1\), then every child \(c\in cs\) is a literal, i.e. \(c = \mathrm{lit}\, l\) for some literal \(l\).
If a gate node \(\mathrm{node}\, \mathit{isAnd}\, cs\) has depth at most \(2\), then every child \(c\in cs\) has depth at most \(1\).
Converts a depth-\(\le 1\) AND subcircuit to a term (a conjunction): a single literal becomes the one-element term, and an AND node becomes the list of its literal children translated via \(\mathrm{toLiteral}\).
Converts a list of children \(cs\) of a top OR gate (of depth \(\le 2\)) into a DNF: each literal child becomes a singleton term, each AND child becomes the term of its literals, and each OR child contributes the singleton terms of its literals.
Converts a list of children \(cs\) of a top AND gate (of depth \(\le 2\)) into a CNF: each literal child becomes a singleton clause, each OR child becomes the clause of its literals, and each AND child contributes the singleton clauses of its literals.
If the top OR node \(\mathrm{node}\, \texttt{false}\, cs\) has depth at most \(2\), then the DNF \(\mathrm{depth2OrToDNF}\, cs\) computes the same Boolean function as the circuit: \((\mathrm{depth2OrToDNF}\, cs).\mathrm{eval}\, x = (\mathrm{node}\, \texttt{false}\, cs).\mathrm{eval}\, x\) for all \(x\).
If the top AND node \(\mathrm{node}\, \texttt{true}\, cs\) has depth at most \(2\), then the CNF \(\mathrm{depth2AndToCNF}\, cs\) computes the same Boolean function as the circuit: \(\mathrm{CNF.eval}\, (\mathrm{depth2AndToCNF}\, cs)\, x = (\mathrm{node}\, \texttt{true}\, cs).\mathrm{eval}\, x\) for all \(x\).
If the top OR node \(\mathrm{node}\, \texttt{false}\, cs\) has depth at most \(2\), the resulting DNF has width at most the maximum fan-in of the circuit: \((\mathrm{depth2OrToDNF}\, cs).\mathrm{width} \le (\mathrm{node}\, \texttt{false}\, cs).\mathrm{maxFanin}\).
If the top AND node \(\mathrm{node}\, \texttt{true}\, cs\) has depth at most \(2\), the resulting CNF has width at most the maximum fan-in of the circuit: \(\mathrm{CNF.width}\, (\mathrm{depth2AndToCNF}\, cs) \le (\mathrm{node}\, \texttt{true}\, cs).\mathrm{maxFanin}\).