NumberSAT

A Boolean formula is a finite expression built from variables, the constants $\mathrm{\top },\mathrm{\perp }$, and the connectives $\mathrm{\neg },\wedge ,\vee$. Under an assignment of zeros and ones to its variables, evaluate constants as one and zero, negation as complementation, conjunction as minimum, and disjunction as maximum. An assignment satisfies the formula when its value is one. Fix an effective binary encoding of these expression trees and finite lists of variable names.

An input to $\mathrm{N}\mathrm{u}\mathrm{m}\mathrm{b}\mathrm{e}\mathrm{r}\mathrm{S}\mathrm{A}\mathrm{T}$ is well formed when it encodes a Boolean formula $\phi$ together with an ordered list $(x_1,\dots ,x_n)$ of distinct variables and every variable occurring in $\phi$ appears in that list. Its value is the exact number of assignments $a:\{x_1,\dots ,x_n\}\to \{0,1\}$ that satisfy $\phi$. Declared variables count even when unused, so the count ranges over all $2^n$ assignments to the list. Every input not having this form is malformed and has value zero.