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 language | English (US) |
---|---|
Pages (from-to) | 292-305 |
Number of pages | 14 |
Journal | LECTURE NOTES IN COMPUTER SCIENCE |
Volume | 3542 |
DOIs | |
State | Published - 2005 |
Event | 7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004 - Vancouver, BC, Canada Duration: May 10 2004 → May 13 2004 |
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- General Computer Science