How Many Solutions Does a SAT Instance Have?
View/
Date
2004-05Citation
P. Pari, L. Yuan, and G. Qu. "How Many Solutions Does a SAT Instance Have?" IEEE International Symposium on Circuits and Systems, Vol. 5, pp. 209-212, May 2004.
Metadata
Show full item recordAbstract
Our goal is to investigate the solution space of a given Boolean
Satisfiability (SAT) instance. In particular, we are interested in determining
the size of the solution space – the number of truth assignments
that make the SAT instance true – and finding all such
truth assignments, if possible. This apparently hard problem has
both theoretical and practical values. We propose an exact algorithm
based on exhaustive search that Solves the instance Once
and Finds All Solutions (SOFAS) and several sampling techniques
that estimate the size of the solution space. SOFAS works better
for SAT instances of small size with a 5X-100X speed-up over the
brute force search algorithm. The sampling techniques estimate
the solution space reasonably well for standard SAT benchmarks.