A deterministic approximation scheme for counting read twice CNF assignments

We give a deterministic fully polynomial time approximation scheme for the number of satisfying assignments of an unweighted Boolean CNF formula in which each variable has at most two literal occurrences. Literal signs and clause lengths are unrestricted. The running time is polynomial in the explicit input size, the reciprocal accuracy, and the encoding length of the accuracy parameter, with a universal exponent. The algorithm uses exact prefix-conditioned dangling-literal recurrences. In the coordinate y = 1/p - 1, every positive marginal has a polynomially bounded coordinate, and the local derivatives satisfy a degree-independent square-root budget. We expand only positive-dependence edges within each computation block, fixing negative-dependence boundary inputs before computing derivative weights. Those weights then allocate accuracy to recursive boundary calls. A joint interpolation estimate and an accuracy-density induction bound both the approximation error and the total work. We give a cancellation-aware rational-arithmetic implementation and a private-literal reduction from counting to marginal approximation. The result combines with the established hardness at three occurrences to give a sharp occurrence boundary for deterministic approximate counting, unless P = NP.