SAT 2004 START ConferenceManager    


A Comparative Study of 2QBF Algorithms

Darsh P. Ranjan, Daijue Tang, Sharad Malik

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


Abstract

A 2QBF problem is the problem of evaluating a Quantified Boolean Formula (QBF) with two levels of quantification. Many practical problems in sequential verification can be formulated as 2QBF. Techniques that are not applicable to general QBF evaluation may be useful for 2QBF evaluation. Particularly, decision order in search based algorithms may not obey quantification order for 2QBF algorithms. Different branching strategies in search based algorithms together with a resolution based method are described and compared. Experimental results on both random benchmarks and 2QBFs formulated from sequential circuit state space diameter problems are analyzed. Experiments show solvers specially tuned for 2QBF can be more efficient than similar general QBF solvers.


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com