Name
Abstract | ||
|---|---|---|
The best currently available solvers for Quantified Boolean Formulas (QBFs) process their input in prenex form, i.e., all the quantifiers have to appear in the prefix of the formula separated from the purely propositional part representing the matrix. However, in many QBFs deriving from applications, the propositional part is intertwined with the quantifier structure. To tackle this problem, the standard approach is to convert such QBFs in prenex form, thereby loosing structural information about the prefix. In the case of search based solvers, the prenex form conversion introduces additional constraints on the branching heuristic, and reduces the benefits of the learn- ing mechanisms. In this paper we show that conversion to prenex form is not necessary: current search based solvers can be nat- urally extended in order to handle non prenex QBFs and to exploit the original quantifier structure. We highlight the two mentioned drawbacks of the conversion in prenex form with a simple example, and we show that our ideas can be useful also for solving QBFs in prenex form. To validate our claims, we implemented our ideas in the state- of-the-art search based solver QUBE, and conducted an extensive experimental analysis. The results show that very substantial speedups can be obtained. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1109/TCAD.2006.888264 | IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems |
Keywords | Field | DocType |
prenex form,search-based procedures,nonprenex qbfs,current search-based solvers,quantified boolean formulas,original quantifier structure,propositional part,state-of-the-art search,state-of-the-art search-based solver,available solvers,search-based solvers,quantifier structure,search space,current search,prenex-form conversion,non prenex qbfs,polynomials,computability,experimental analysis,knowledge representation,space exploration,propulsion,boolean functions,formal verification,encoding | Boolean function,Knowledge representation and reasoning,Polynomial,Computer science,Matrix (mathematics),Parallel computing,Algorithm,Computability,Prefix,Theoretical computer science,Solver,Formal verification | Journal |
Volume | Issue | ISSN |
26 | 3 | 1530-1591 |
ISBN | Citations | PageRank |
3-9810801-0-6 | 18 | 0.80 |
References | Authors | |
35 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Enrico Giunchiglia | 1 | 2380 | 164.28 |
| Massimo Narizzano | 2 | 451 | 30.41 |
| Armando Tacchella | 3 | 1448 | 108.82 |