In this paper, we present an efficient algorithm for a satisfiable CNF formula that has tradeoff between time and the number of satisfying assignments. The algorithm is based on the inclusion-exclusion principle for counting the number of unsatisfying assignments and its tight approximation. We first construct a decision algorithm whether a given formula is satisfiable or not. Then, by using it as a subroutine, we construct an algorithm for finding one satisfying assignment. When a given formula contains a variables, m clauses, and 2{sup}n/δ satisfying assignments, it runs in 2{sup{O({the square root of m}log(3/2) mlogδ) time. For the case m = o(n{sup}(2 - ε) and δ = 2{sup}(n{sup}ε) (0 ≤ ε < 1), it achieves subexponential time.
展开▼
