A satisfying assignment makes every clause of a CNF formula true. For a specified declared variable list, #F means the number of distinct assignments that satisfy F. It counts assignments, not true clauses. For F = (p OR q) AND (NOT p) over p, q, only p = false and q = true works, so #F = 1. If an unused variable r is also declared, either value of r works and #F = 2. Exact counting returns this integer, not an estimate.