How Many Solutions Does a SAT Instance Have?

Loading...
Thumbnail Image

Files

c038.pdf (304.29 KB)
No. of downloads: 565

Publication or External Link

Date

2004-05

Advisor

Citation

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.

DRUM DOI

Abstract

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.

Notes

Rights