Home People Papers Tool Description

Welcome! Keywords: the counting SAT problem, approximation, polynomial time complexity An extension of the SAT problem is the counting SAT problem which is to count how many satisfying assignments there are for a SAT problem. Counting SAT (#SAT) is used in problems such as knowledge compilation, probabilistic reasoning, program verification, computing the permanent of a boolean matrix, etc. Counting SAT is a difficult problem which is at least as hard as NP-complete problems but probably much harder. One of the best recent counting SAT solvers is Cachet by Sang, Beame and Kautz. However exact counting SAT is still very expensive the moment the propositional formulas become larger, i.e. thousands of variables and clauses. This paper provides an alternative approach — we provide a fast approximation of the of the number of solutions. Our technique is based on successive variable and clause elimination. Experimental results demonstrate that our technique is promising. For large formulae, our initial show large speedups compared with Cachet, by providing an approximate count instead of the exact count.