Disjoint SAT Counting as a Coproduct Decomposition: A Rust Prototype
Author: Anonymous
Abstract
We describe a deterministic exact model counter for finite CNF formulas that implements the disjoint sparsification step of OpenAI's 2026 SAT manuscript and counts the resulting leaves by DPLL. We formulate each split as a coproduct of satisfying-assignment objects, prove the mathematical partition and a conditional correctness result for the algorithm, and report bounded differential tests. This prototype does not implement the source's subexponential algebraic leaf counter; its running time is not claimed to satisfy the source theorem.
1. Problem and scope
Let $V=\{1,\ldots,n\}$ be the declared variables. A literal is $x_i$ or $\neg x_i$, a clause is a finite disjunction of literals, and a CNF formula $F$ is a finite conjunction of clauses. Its set of models and exact count are
$$\operatorname{Sat}_V(F)=\{x\in\{0,1\}^{V}:F(x)=1\},\qquad \#_V F=|\operatorname{Sat}_V(F)|.$$
The declared universe matters: a variable absent from all clauses remains free and doubles the model count. The empty conjunction is true; an empty clause is false. We implement the disjoint branching construction of [1, Appendix A], with a different leaf solver. The pinned Lean result [2] states a subexponential-time, polynomial-space existence theorem for a fixed-width primitive machine. Our Rust program neither extracts that machine nor establishes its resource bounds. The original proof and its interpretation are not independently verified here.
2. The disjoint split
Assume the formula has been normalized by deleting repeated literals, tautological clauses, duplicates, and clauses containing another clause. Choose a nonempty set $H$ of literals and all width-$c$ clauses of the form $H\cup P_a$; $H$ is a proper subset of each such clause. Write $G$ for the conjunction of all other clauses. The two children are
$$F_A=G\wedge\bigvee_{\ell\in H}\ell,\qquad F_B=G\wedge\bigwedge_a\bigvee_{p\in P_a}p\wedge\bigwedge_{\ell\in H}\neg\ell.$$
Proposition 1 (partition). There is a canonical bijection
$$\operatorname{Sat}_V(F_A)\sqcup\operatorname{Sat}_V(F_B)\;\cong\;\operatorname{Sat}_V(F).$$
Proof. If an assignment satisfies $H$, every selected clause is true, so the assignment satisfies the original formula exactly when it satisfies $G$, hence $F_A$. Otherwise every literal of $H$ is false, so each selected clause has the same truth value as its residual clause $P_a$; the assignment satisfies $F$ exactly when it satisfies $F_B$. These cases are exhaustive and disjoint. Normalizing either child preserves its truth value. ∎
Corollary 2 (counting). $\#_V F=\#_V F_A+\#_V F_B$. This remains valid with free variables because neither child changes $V$.
The implementation chooses the smallest eligible clause width $c$, then a largest eligible core $H$, with deterministic tie-breaking, subject to $\deg_c(H)\ge M^{c-|H|}$ for a chosen integer $M\ge2$. It processes the tree depth first. Along every edge the vector of numbers of clauses of each width, ordered from the largest width down, strictly decreases lexicographically: selected width-$c$ clauses disappear, new clauses have smaller width, and normalization only removes clauses. Thus the split tree terminates. This elementary termination argument does not by itself supply the source's subexponential cost bound.
3. Categorical reading
An assignment is an element of the finite set $X=2^V$, and a formula determines a subobject $\operatorname{Sat}_V(F)\hookrightarrow X$. The two cases in Proposition 1 are complementary subobjects, so the displayed bijection is a coproduct decomposition in $\mathbf{FinSet}$. Applying cardinality sends that coproduct to addition in $\mathbb N$. Relabeling variables by a bijection transports all three model sets and makes the partition bijection commute with relabeling.
The same logical decomposition can be interpreted in any Boolean elementary topos: interpret valuations in $2^V$, literals as subobjects, and $H$ and its complement as complementary subobjects. Distributivity gives the internal isomorphism $[F]\cong[F\wedge H]\amalg[F\wedge\neg H]$, and the residual-clause identities identify the two terms with $[F_A]$ and $[F_B]$. This is a Boolean-topos statement; ordinary finite cardinality and the displayed natural-number count are asserted only in $\mathbf{FinSet}$. No specifically higher-categorical or homotopical speedup is claimed.
4. Counting the leaves
At a leaf, the implementation uses depth-first DPLL. Unit propagation fixes an unassigned variable only when a currently unsatisfied clause has exactly one unassigned literal. A conflicting clause contributes zero. Otherwise it branches on a variable occurring in an unsatisfied clause, adding the two disjoint conditional counts. When all clauses are true, it contributes $2^u$, where $u$ is the number of still-unassigned declared variables. The accumulator is an arbitrary-precision natural number.
Proposition 3 (mathematical correctness). Assuming exact integer operations, correct representation of the input, and the stated implementations of normalization, splitting, and DPLL, the algorithm returns $\#_V F$.
Proof. Unit propagation preserves all satisfying extensions, a false clause has none, and the two values of a branch variable partition the satisfying extensions. When all clauses hold, every assignment of the $u$ remaining variables is valid. Induction on the number of unassigned variables proves correctness of the leaf count. Proposition 1 and induction on the finite split tree then prove the result for the root. ∎
This is a proof of the specified mathematical algorithm, conditional on the Rust code implementing it correctly; it is not a machine-checked proof of the Rust program. The program rejects normalized widths above 12 in sparse mode to control subset enumeration; the direct DPLL and exhaustive modes have no such width cap.
5. Reproduction and limits
The provided Rust package accepts DIMACS CNF and can be tested with cargo test --offline -- --nocapture. In one run with Rust 1.99.1 on x86-64 Linux, the five test functions passed. They include 3,200 deterministic small-formula differential cases against exhaustive assignment enumeration, including 4,400 sparse-counter invocations across two thresholds. Of these, the 2,000 nonempty-formula cases exercised 806 sparsification splits. Tests also cover an empty variable universe, contradictory units, tautologies, unused variables, malformed input, and the output $2^{1000}$. The example $(x_1\lor x_2)\land(\neg x_1\lor x_3)$ with a fourth free variable returns 8. A separate Python script generated 500 seeded small formulas and compared both compiled CLI methods with a Python exhaustive oracle; all comparisons passed.
The tests are finite, and their counter and oracle share infrastructure for arbitrary-precision accumulation. They do not rule out bugs. No competitive performance experiment was performed. In particular, the fast sparse-polynomial common-zero counter, replacement-form construction, greedy hashes, and Taylor-interpolation path from [1] are absent. The implementation can take exponential time and does not refute ETH or prove any complexity separation. The upstream authors' claims are attributed to them and are subject to external examination [3].
There is also a striking finite-size feature of the paper's stated interpolation schedule. For $20\le n\le2^{64}$, let $\lambda=\lceil\log_2 n\rceil$, $\nu=\lceil\log_2\lambda\rceil$, and $s=\lfloor\sqrt\lambda/\nu^2\rfloor$, as in [1, “Returning to a general formula”]. Then $5\le\lambda\le64$ and $\nu\ge3$, so $\sqrt\lambda/\nu^2\le8/9<1$, hence $s=0$. The paper's specified $s<2$ fallback is therefore selected throughout this range. This calculation concerns that stated schedule; it does not rule out other parameter choices, implementations, or future practical speedups.
6. Provenance and references
This work was prepared at a user's direction with OpenAI Codex assistance for code, tests, and manuscript drafting. The author requests an anonymous byline; no claim of independent human verification is made. Reviewers should evaluate the evidence and source directly.
1. OpenAI, The Exponential Time Hypothesis is False, 25 October 2026, pinned manuscript.
2. OpenAI, Lean theorem Final.lean, and formalization scope, pinned to the same commit.
3. OpenAI, Working with academic communities to build scientific understanding, 26 October 2026.