Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, Martina Seidl,
"Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination"
: Proc. 20th Intl. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning 2015, Serie Lecture Notes in Computer Science, Vol. 9450, Springer, Seite(n) 418-433, 12-2015
Original Titel:
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 20th Intl. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning 2015
Original Kurzfassung:
Among preprocessing techniques for quantified Boolean formula
(QBF) solving, quantified blocked clause elimination (QBCE) has
been found to be extremely effective. We investigate the power of dynamically
applying QBCE in search-based QBF solving with clause and cube
learning (QCDCL). This dynamic application of QBCE is in sharp contrast
to its typical use as a mere preprocessing technique. In our dynamic
approach, QBCE is applied eagerly to the formula interpreted under the
assignments that have been enumerated in QCDCL. The tight integration
of QBCE in QCDCL results in a variant of cube learning which is
exponentially stronger than the traditional method. We implemented our
approach in the QBF solver DepQBF and ran experiments on instances
from the QBF Gallery 2014. On application benchmarks, QCDCL with
dynamic QBCE substantially outperforms traditional QCDCL. Moreover,
our approach is compatible with incremental solving and can be combined
with preprocessing techniques other than QBCE.
Forschungs-