REVIEW
The CNF Encoding Complexity of Boolean Functions
Computational Complexity · Submitted 3 Nov 2026 · 70 references
Pith's verdict: Strong and ambitious paper with a gap in Lemma 11 that needs patching before the main claim holds as stated.
T0 · AI review
Why Pith says this
Highlight any text to comment on it.
Referee report
The paper
The paper claims
If a Boolean function can be evaluated by a nondeterministic RAM with m advice bits of which at most b are accessed per input, then it admits a CNF encoding with Õ(t + √(mb)) clauses.
The reading
What carries the argument
The mass-production lemma (Lemma 11) is the central technical engine. It encodes b simultaneous queries to a Boolean function g (with truth table of size 2^k) using only Õ(√(b·2^k)) clauses. The construction uses an explicit bipartite expander graph (from Teutsch) to assign each query to one of O(b) slots such that any small set of queries can be matched to distinct slots. For each slot r, a sparse function g_r is defined as g restricted to the neighborhood of r; because each g_r has few satisfying inputs, it can be encoded compactly via Lemma 13 (a sparse-function encoding). The conjunction of these slot-level encodings, together with a simple verification formula, achieves the claimed bound. This lemma is the key to reducing the advice-query component of Theorem 2 from the naive O(b√m) down to O(√(mb)).
Extended reading notes
Core claim
The paper's core discovery is that the CNF encoding complexity of a Boolean function is governed by the product √(mb) rather than by m alone, when the function is computed by a nondeterministic RAM that reads at most b advice bits per input. This is captured by Theorem 2: enc(f) = Õ(t + √(mb)). The proof introduces a mass-production lemma (Lemma 11) that encodes b queries to an arbitrary function g with Õ(√(b·2^k)) clauses—far fewer than the b·2^k clauses that a naive scheme would require. This lemma relies on Teutsch's explicit expander to hash the b queries into slots, creating sparsity that is exploited by a separate sparse-function encoding (Lemma 13). The paper also sharpens the bound for sparsely supported functions (Theorem 6): enc(n,M) = Θ(n + √(M(n − lg M))), and it characterizes encoding complexity exactly as the minimum number of ∧-gate wires in a nondeterministic De Morgan circuit (Proposition 44).
Load-bearing premise
The mass-production lemma (Lemma 11) assumes the existence of an explicit expander graph (from Teutsch, Lemma 14) that guarantees a Hall-type matching condition for any set of at most b query indices; if such an expander did not exist for the required range of parameters, the main theorem's bound would not be achievable.
Editorial extensions
If this is right
- If Theorem 2 is correct, then any NP-complete problem that admits a nondeterministic algorithm with low-advice access can be reduced to CNF-SAT with asymptotically fewer clauses than by standard reductions. This could lead to smaller SAT instances for problems like Hamiltonian cycle and k-clique, where the paper gives explicit corollaries (Corollaries 7 and 8).
- The application to k-CNF functions (Theorem 4) shows that the encoding size is n^k / 2^{Ω_k(√(log n))}, which is exponentially smaller than the naive O(n^k) and beats the previous best O(n^k / log n) by a subexponential factor. This suggests that unbounded-width clauses are genuinely more powerful than bounded-width ones for representing k-CNF functions, since a counting argument shows that bounde
- The polynomial-time construction (Theorem 5) gives a concrete, efficiently computable encoding with O_k(n^k (log log n)^3 / log^2 n) clauses. This is immediately usable in SAT-based tools that need to produce compact encodings of k-CNF constraints.
- The characterization by nondeterministic De Morgan circuits (Proposition 44) links encoding complexity to a natural circuit measure, potentially opening the door to lower-bound techniques from circuit complexity.
Reading between the lines
- The mass-production lemma (Lemma 11) may find applications beyond CNF encodings: it shows that b queries to a table of size 2^k can be verified using only Õ(√(b·2^k)) constraints. This could be useful in interactive proofs, PCP constructions, or any setting where multiple lookups need to be compressed.
- The derandomization of the Larsen–Williams data structure (Section 4.1) is interesting in its own right: it provides a deterministic data structure for independent-set queries with O(n^2) space and query time n^2 / 2^{Ω(√(log n))}. This may improve worst-case upper bounds for other fine-grained problems.
- The sharp bound for sparse functions (Theorem 6) suggests that encoding complexity is essentially determined by the support size and the number of variables, which may help in designing optimal encodings for specific sparse Boolean functions arising in practice.
Original abstract
We study the minimum number of clauses required to encode a boolean function into a CNF formula with auxiliary variables. Our main result is that if a boolean function can be evaluated in nondeterministic time $t$ (in the RAM model) with $m$ bits of advice such that at most $b$ bits of advice are accessed for each input, then it admits a CNF encoding with $\widetilde{O}(t + \sqrt{mb})$ clauses. This constitutes a nonuniform generalization of Robson's (TCS'91) variant of the Cook--Levin theorem, for which a na\"ive generalization would yield $\widetilde{O}(t+m)$ clauses; our applications leverage $b = o(m)$ to obtain significantly better bounds. Since preprocessed data structures can be modeled as computation with advice, our result allows us to translate space- and time-efficient data structures to compact CNF encodings. As an application, we derandomize a data structure of Larsen and Williams (SODA'17) to show that every $k$-CNF function on $n$ inputs can be encoded with $n^k/2^{\Omega_k(\sqrt{\lg n})}$ clauses. Notably, despite encoding a $k$-CNF function, the encoding itself necessarily contains clauses of unbounded width, since an information-theoretic argument shows that the minimum number of bounded-width clauses to encode such functions is $\Omega_k(n^{k}/\lg n)$ in the worst case. In general terms, our results imply that for a wide variety of NP-complete problems, one can reduce to CNF-SAT in a way that results in asymptotically fewer clauses than previously known methods.
The compiled record
The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
The abstract, sentence by sentence
We study the minimum number of clauses required to encode a boolean function into a CNF formula with auxiliary variables. Our main result is that if a boolean function can be evaluated in nondeterministic time $t$ (in the RAM model) with $m$ bits of advice such that at most $b$ bits of advice are accessed for each input, then it admits a CNF encoding with $\widetilde{O}(t + \sqrt{mb})$ clauses. This constitutes a nonuniform generalization of Robson's (TCS'91) variant of the Cook--Levin theorem, for which a na\"ive generalization would yield $\widetilde{O}(t+m)$ clauses; our applications leverage $b = o(m)$ to obtain significantly better bounds. Since preprocessed data structures can be modeled as computation with advice, our result allows us to translate space- and time-efficient data structures to compact CNF encodings. As an application, we derandomize a data structure of Larsen and Williams (SODA'17) to show that every $k$-CNF function on $n$ inputs can be encoded with $n^k/2^{\Omega_k(\sqrt{\lg n})}$ clauses. Notably, despite encoding a $k$-CNF function, the encoding itself necessarily contains clauses of unbounded width, since an information-theoretic argument shows that the minimum number of bounded-width clauses to encode such functions is $\Omega_k(n^{k}/\lg n)$ in the worst case. In general terms, our results imply that for a wide variety of NP-complete problems, one can reduce to CNF-SAT in a way that results in asymptotically fewer clauses than previously known methods.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | We study the minimum number of clauses required to encode a boolean function into a CNF formula with auxiliary variables. | background 0.61 | 0.71 | 0.02 | asserted 0.63 |
| s1 | Our main result is that if a boolean function can be evaluated in nondeterministic time $t$ (in the RAM model) with $m$ bits of advice such that at most $b$ bits of advice are accessed for each input, then it admits a CNF encoding with $\widetilde{O}(t + \sqrt{mb})$ clauses. | result 0.99 | 0.94 | 0.98 | asserted 1.00 |
| s2 | This constitutes a nonuniform generalization of Robson's (TCS'91) variant of the Cook--Levin theorem, for which a na\"ive generalization would yield $\widetilde{O}(t+m)$ clauses; our applications leverage $b = o(m)$ to obtain significantly better bounds. | interpretation 0.78 | 0.36 | 0.09 | asserted 1.00 |
| s3 | Since preprocessed data structures can be modeled as computation with advice, our result allows us to translate space- and time-efficient data structures to compact CNF encodings. | interpretation 0.97 | 0.62 | 0.03 | asserted 0.75 |
| s4 | As an application, we derandomize a data structure of Larsen and Williams (SODA'17) to show that every $k$-CNF function on $n$ inputs can be encoded with $n^k/2^{\Omega_k(\sqrt{\lg n})}$ clauses. | result 0.91 | 0.93 | 0.04 | asserted 1.00 |
| s5 | Notably, despite encoding a $k$-CNF function, the encoding itself necessarily contains clauses of unbounded width, since an information-theoretic argument shows that the minimum number of bounded-width clauses to encode such functions is $\Omega_k(n^{k}/\lg n)$ in the worst case. | limitation 0.50 | 0.82 | 0.04 | asserted 1.00 |
| s6 | In general terms, our results imply that for a wide variety of NP-complete problems, one can reduce to CNF-SAT in a way that results in asymptotically fewer clauses than previously known methods. | interpretation 1.00 | 0.78 | 0.08 | asserted 0.75 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
Figures
Figures reproduced from arXiv:2611.05614 by the authors.
References
Discussion
Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.