Approximate Satisfiability Counting

The problem of counting satisfiability, i.e. count the number of satisfying assignments for a SAT problem, is used successfully in a number of problems. For example, it can provide heuristics for guiding planning and search, where an estimation of the probability for a given search would help lead to a goal. Counting satisfiability is a valuable approach for problems like constraint satisfaction, knowledge compilation, probabilistic reasoning and computing the permanent of a Boolean matrix. The difficulty with counting satisfiability is that it is as hard as NP-complete problems, but probably much harder. This means that solvers to count the exact number of solutions may need a large amount on time on large prepositional formulas. In this paper, we provide a fast alternative by approximating the number of instances. Our technique is based on successive variable and clause elimination. Experimental results demonstrate that our technique is promising.