Name
Abstract | ||
|---|---|---|
During the recent years, the development of tools for deciding Quantified Boolean Formu- las (QBFs) has been accompanied by a steady supply of real-world instances, i.e., QBFs originated by translations from application domains. Instances of this kind showed to be challenging for current state-of-the-art QBF solvers, while the ability to deal effectively with them is necessary to foster adop- tion of QBF-based reasoning in practice. In this paper we describe three reasoning techniques that we implemented in our solver QUBE++ to increase its performances on real-world instances coming from formal verification and planning domains. We present experimental results that witness the contribu- tion of each technique and the better performances of QUBE++ with respect to other state-of-the-art QBF solvers. The effectiveness of QUBE++ is further confirmed by experiments run on challenging real-world SAT instances, where QUBE++ turns out to be competitive with respect to current state-of- the-art SAT solvers. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/11527695_9 | SAT |
Keywords | Field | DocType |
state-of-the-art solver,monotone literal,specialized solvers,qube performance,qbf reasoning,qbf evaluation,quantified boolean formulas,efficient detection,real-world instance,important technique,current state-of-the-art qbf solvers,formal verification,sat solver | Discrete mathematics,Constraint satisfaction,Computer science,Heuristics,Conjunctive normal form,Boolean algebra,Formal methods,Solver,True quantified Boolean formula,Formal verification | Conference |
Volume | ISSN | ISBN |
3542 | 0302-9743 | 3-540-27829-X |
Citations | PageRank | References |
8 | 0.64 | 26 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Enrico Giunchiglia | 1 | 2380 | 164.28 |
| Massimo Narizzano | 2 | 451 | 30.41 |
| Armando Tacchella | 3 | 1448 | 108.82 |