Analysis of search based algorithms for satisfiability of propositional and quantified boolean formulas arising from circuit state space diameter problems

Daijue Tang, Yinlei Yu, Darsh Ranjan, Sharad Malik

Research output: Contribution to journalConference article

2 Scopus citations

Abstract

The sequential circuit state space diameter problem is an important problem in sequential verification. Bounded model checking is complete if the state space diameter of the system is known. By unrolling the transition relation, the sequential circuit state space diameter problem can be formulated as either a series of Boolean satisfiability (SAT) problems or an evaluation for satisfiability of a Quantified Boolean Formula (QBF). Thus far neither the SAT based technique that uses sophisticated SAT solvers, nor QBF evaluations for the various QBF formulations for this have fared well in practice. The poor performance of the QBF evaluations is blamed on the relative immaturity of QBF solvers, with hope that ongoing research in QBF solvers could lead to practical success here. Most existing QBF algorithms, such as those based on the DPLL SAT algorithm, are search based. We show that using search based QBF algorithms to calculate the state space diameter of sequential circuits with existing problem formulations is no better than using SAT to solve this problem. This result holds independent of the representation of the QBF formula. This result is important as it highlights the need to explore non-search based or hybrid of search and non-search based QBF algorithms for the sequential circuit state space diameter problem.

Original languageEnglish (US)
Pages (from-to)292-305
Number of pages14
JournalLECTURE NOTES IN COMPUTER SCIENCE
Volume3542
DOIs
StatePublished - 2005
Event7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004 - Vancouver, BC, Canada
Duration: May 10 2004May 13 2004

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Analysis of search based algorithms for satisfiability of propositional and quantified boolean formulas arising from circuit state space diameter problems'. Together they form a unique fingerprint.

  • Cite this