Integrating Dependency Schemes in Search-Based QBF Solvers
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10)
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
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-