Inclusion-exclusion for k-CNF formulas
We show that the number of satisfying assignments of a k-CNF formula is determined uniquely from the numbers of unsatisfying assignments for clause-sets of size up to [log k] + 2. This amount of information is also shown to be necessary. (C) 2003 Elsevier Science B.V. All rights reserved.
inclusion-exclusion k-cnf formula combinatorial problems sat counting