How many solutions does a SAT instance have?

Author

Pari, Pushkin R. ; Yuan, Lin ; Qu, Gang

Author_Institution

Dept. of Electr. & Comput. Eng., Maryland Univ., College Park, MD, USA

Volume

5

fYear

2004

fDate

23-26 May 2004

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.

Keywords

Boolean algebra; computability; computational complexity; search problems; Boolean satisfiability; SOFAS; brute force search algorithm; sampling techniques; solution space; truth assignments; Application software; Automatic test pattern generation; Computer science; Design optimization; Educational institutions; Logic design; Logic testing; Sampling methods; Space exploration; Very large scale integration;

fLanguage

English

Publisher

ieee

Conference_Titel

Circuits and Systems, 2004. ISCAS '04. Proceedings of the 2004 International Symposium on

Print_ISBN

0-7803-8251-X

Type

conf

DOI

10.1109/ISCAS.2004.1329499

Filename

1329499