Name
Title | ||
|---|---|---|
Analysis of search based algorithms for satisfiability of propositional and quantified boolean formulas arising from circuit state space diameter problems |
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. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/11527695_23 | SAT (Selected Papers |
Keywords | Field | DocType |
important problem,qbf evaluation,state space diameter,diameter problem,various qbf formulation,qbf algorithm,qbf formula,qbf solvers,sequential circuit state space,existing qbf algorithm,circuit state space diameter,boolean formula,sat solver,state space,sequential circuits,satisfiability,boolean satisfiability | Discrete mathematics,Model checking,Computer science,Boolean satisfiability problem,Algorithm,Binary decision diagram,DPLL algorithm,Conjunctive normal form,Boolean algebra,True quantified Boolean formula,State space | Conference |
Volume | ISSN | ISBN |
3542 | 0302-9743 | 3-540-27829-X |
Citations | PageRank | References |
13 | 0.75 | 23 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daijue Tang | 1 | 40 | 2.42 |
| Yinlei Yu | 2 | 95 | 5.96 |
| Darsh Ranjan | 3 | 13 | 0.75 |
| Sharad Malik | 4 | 7766 | 691.24 |