A Comparative Study of 2QBF Algorithms

2QBF 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 instances of 2QBF. Techniques that are not applicable to general QBF evaluation may be useful for 2QBF evaluation. In particular, decision order in search based algorithms may not obey quantification order for 2QBF evaluation 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.

• Type: Conference
• Year: 2004
• Where: SAT
• Authors: Darsh P. Ranjan, Daijue Tang, Sharad Malik
• Keywords: General Qbf Evaluation, Quantified Boolean Formula, SAT 2004, Search Based Algorithms