Read/Search this Article
The number of satisfying assignments of k-CNF formulas is computed using the inclusion-exclusion formula for sets of clauses. Recently, it was shown that the information on the sets of clauses of size ≤ ⌊log k⌋ + 2 already uniquely determines the number of satisfying assignments of k-CNF formulas . The proof was, however, only existential and no explicit procedure was presented. In this paper, we show that such a procedure exists.