The Cook--Levin construction can be made parsimonious

Replace $N$ by a fixed one-tape simulator $N^{\ast }$. Between two transitions of $N$, the simulator's sweeps are deterministic; at an original nondeterministic transition it makes exactly the same tagged choice as $N$. Each such choice first enters a distinct intermediate state labelled by its transition tag, before deterministically executing that transition; these states are part of the recorded configuration. Even choices with the same eventual successor therefore give different tableau rows. Erasing the deterministic simulation steps and reading these tags is a bijection between accepting paths. The standard multitape-to-one-tape simulation has polynomial slowdown. Choose a polynomial $T(n)\ge n+1$ bounding both its running time and every tape position it can visit, and pad every halted branch to time $T(n)$. This supplies all hypotheses of [L1]--[L3].

Use one-hot tableau variables for the symbol (including the tagged state) in every time-cell position. The initial-row, exactly-one-symbol, local-transition, and accepting constraints use only those variables. Take their conjunction as ${\phi }_{N,x}$ without introducing auxiliary variables. Let $V_{N,x}$ list every cell variable $X_{t,c,a}$ once, in lexicographic order of time, cell, and a fixed order on the simulator alphabet. Output the encoded pair $({\phi }_{N,x},V_{N,x})$, which is well formed for NumberSAT.

An accepting path fixes every cell of its padded tableau and therefore one truth value for every tableau variable. Every declared variable is such a cell variable, so none contributes a free choice. Conversely, any satisfying assignment gives exactly one legal accepting tableau by [L2], and the retained choice tags recover exactly one accepting path of $N^{\ast }$, hence exactly one accepting path of $N$ by step 1.1. These maps are inverse, so $\mathrm{\#}{\mathrm{acc}}_N(x)=\mathrm{N}\mathrm{u}\mathrm{m}\mathrm{b}\mathrm{e}\mathrm{r}\mathrm{S}\mathrm{A}\mathrm{T}({\phi }_{N,x},V_{N,x})\mathrm{.}$

The tableau has polynomial dimensions, its local constraints have polynomial total size, and [L3] supplies the polynomial-time construction. Enumerating the polynomially many declared variable names in the specified order also takes polynomial time. Together with the exact equality in step 3.1, [L4] proves parsimony.