All-SAT using minimal blocking clauses

Yinlei Yu, Pramod Subramanyan, Nestan Tsiskaridze, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

28 Scopus citations

Abstract

The All-SAT problem deals with determining all the satisfying assignments that exist for a given propositional logic formula. This problem occurs in verification applications including predicate abstraction and unbounded model checking. A typical All-SAT solver is based on iteratively computing satisfying assignments using a traditional Boolean satisfiability (SAT) solver and adding blocking clauses which are the complement of the total/partial assignments. We argue that such an algorithm is doing more work than needed and introduce new algorithms that are more efficient. Experiments show that these algorithms generate solutions with up to 14X fewer partial assignments and are up to three orders of magnitude faster.

Original languageEnglish (US)
Title of host publicationProceedings - 27th International Conference on VLSI Design, VLSID 2014; Held Concurrently with 13th International Conference on Embedded Systems Design
Pages86-91
Number of pages6
DOIs
StatePublished - 2014
Event27th International Conference on VLSI Design, VLSID 2014 - Held Concurrently with 13th International Conference on Embedded Systems Design - Mumbai, India
Duration: Jan 5 2014Jan 9 2014

Publication series

NameProceedings of the IEEE International Conference on VLSI Design
ISSN (Print)1063-9667

Other

Other27th International Conference on VLSI Design, VLSID 2014 - Held Concurrently with 13th International Conference on Embedded Systems Design
Country/TerritoryIndia
CityMumbai
Period1/5/141/9/14

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Keywords

  • All-SAT
  • Reachability
  • SAT
  • SAT solver
  • Verification

Fingerprint

Dive into the research topics of 'All-SAT using minimal blocking clauses'. Together they form a unique fingerprint.

Cite this