How Many Solutions Does a SAT Instance Have?

dc.contributor.authorPari, Pushkin R.
dc.contributor.authorYuan, Lin
dc.contributor.authorQu, Gang
dc.date.accessioned2009-05-11T13:53:36Z
dc.date.available2009-05-11T13:53:36Z
dc.date.issued2004-05
dc.description.abstractOur 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.en
dc.format.extent311595 bytes
dc.format.mimetypeapplication/pdf
dc.identifier.citationP. 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.en
dc.identifier.urihttp://hdl.handle.net/1903/9065
dc.language.isoen_USen
dc.publisherIEEEen
dc.relation.isAvailableAtA. James Clark School of Engineeringen_us
dc.relation.isAvailableAtElectrical & Computer Engineeringen_us
dc.relation.isAvailableAtDigital Repository at the University of Marylanden_us
dc.relation.isAvailableAtUniversity of Maryland (College Park, MD)en_us
dc.rights.licenseCopyright © 2004 IEEE. Reprinted from IEEE International Symposium on Circuits and Systems. This material is posted here with permission of the IEEE. Such permission of the IEEE does not in any way imply IEEE endorsement of any of the University of Maryland's products or services. Internal or personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution must be obtained from the IEEE by writing to pubs-permissions@ieee.org. By choosing to view this document, you agree to all provisions of the copyright laws protecting it.
dc.subjectBoolean Satisfiability (SAT) instanceen
dc.subjectSolves the instance Once and Finds All Solutions (SOFAS)en
dc.titleHow Many Solutions Does a SAT Instance Have?en
dc.typeArticleen

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
c038.pdf
Size:
304.29 KB
Format:
Adobe Portable Document Format
License bundle
Now showing 1 - 2 of 2
No Thumbnail Available
Name:
license.txt
Size:
1.8 KB
Format:
Item-specific license agreed upon to submission
Description:
No Thumbnail Available
Name:
IEEE Permission Qu.txt
Size:
3.7 KB
Format:
Plain Text
Description: