= Quadratic-size formula with prescribed model count
{title2=$|\varphi_k|=O(n^2),\quad\#\operatorname{SAT}(\varphi_k)=k$}
For each $0\leq k\leq2^n$, a <propositional formula> over $n$ specified variables can have exactly $k$ <satisfying assignments> and length $O(n^2)$. For $0<k<2^n$, interpret a <Boolean valuation> as the <binary number> $x_1\cdots x_n$ and test whether it is less than $k=b_1\cdots b_n$.
For every position $i$ with $b_i=1$, use a conjunction asserting that all earlier <bits> equal $b_j$ and $x_i=0$, leaving later <bits> unrestricted. Take the disjunction of these terms. Each satisfying assignment has a unique first differing position, so the terms are disjoint, and their counts sum to $\sum_{i:b_i=1}2^{n-i}=k$. Their combined length is $O(1+2+\cdots+n)=O(n^2)$. Use <logical falsity> and <logical truth> at the two endpoints. The count is over all $n$ variables, including those absent from an individual term or from the whole formula.
Back to article page
