Armin Biere, Florian Lonsing,
"DepQBF: A Dependency-Aware QBF Solver (System Description)"
: Proc. Pragmatics of SAT Workshop (POS'10), 2010
Original Titel:
DepQBF: A Dependency-Aware QBF Solver (System Description)
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. Pragmatics of SAT Workshop (POS'10)
Original Kurzfassung:
We present DepQBF 0.1, a new search-based solver for quantified
boolean formulae (QBF). It integrates compact dependency graphs to
overcome the restrictions imposed by linear quantifier prefixes of
QBFs in prenex conjunctive normal form (PCNF). DepQBF 0.1 was placed
first in the main track of QBFEVAL'10 in a score-based
ranking. We provide a general system overview and describe selected
orthogonal features such as restarts and removal of learnt constraints.
---------------
Vortrag bei der Konferenz: http://ie.technion.ac.il/SAT10/
Titel: "Integrating Dependency Schemes in Search-Based QBF Solvers"
Autoren: Florian Lonsing, Armin Biere
Abstract:
Many search-based QBF solvers implementing the DPLL algorithm for QBF
(QDPLL) process formulae in prenex conjunctive normal form (PCNF). The
quantifier prefix of PCNFs often results in strong variable
dependencies which can influence solver performance negatively. A
common approach to overcome this problem is to reconstruct quantifier
structure e.g.~by quantifier trees. Dependency schemes are a
generalization of quantifier trees in the sense that more general
dependency graphs can be obtained. So far, dependency graphs have not
been applied in QBF solving. In this work we consider the problem of
efficiently integrating dependency graphs in QDPLL. Thereby we
generalize related work on integrating quantifier trees. By analyzing
the core parts of QDPLL, we report on modifications necessary to
profit from general dependency graphs. In comprehensive experiments we
show that QDPLL using a particular dependency graph, despite of
increased overhead, outperforms classical QDPLL relying on quantifier
prefixes of PCNFs.
Forschungs-