NumberSAT belongs to Sharp-P

First check the formula syntax and declared-variable list deterministically; on malformed input reject without making a nondeterministic choice. On a valid input with $n$ declared variables, make exactly $n$ binary choices, interpret them in the declared order as an assignment, evaluate the formula, and accept exactly when it is true.

The $2^n$ computation paths are in bijection with the $2^n$ declared assignments, and a path accepts exactly when its assignment satisfies the formula. At $n=0$ there is one path, corresponding to the empty assignment; malformed input has no accepting path. Thus the accepting-path count is exactly $\mathrm{N}\mathrm{u}\mathrm{m}\mathrm{b}\mathrm{e}\mathrm{r}\mathrm{S}\mathrm{A}\mathrm{T}(\phi )$.

The machine runs in polynomial time, so its counting function belongs to $\mathrm{\#}\mathrm{P}$ by [L1].