Alexandra Goultiaeva, Martina Seidl, Armin Biere,
"Bridging the Gap between Dual Propagation and CNF-based QBF Solving"
: In Proc. Intl. Conf. on Design, Automation & Test in Europe (DATE'13), Seite(n) 811-814, 2013
Original Titel:
Bridging the Gap between Dual Propagation and CNF-based QBF Solving
Sprache des Titels:
Englisch
Original Buchtitel:
In Proc. Intl. Conf. on Design, Automation & Test in Europe (DATE'13)
Original Kurzfassung:
Conjunctive Normal Form (CNF) representation as
used by most modern Quantified Boolean Formula (QBF) solvers
is simple and powerful when reasoning about conflicts, but is not
efficient at dealing with solutions. To overcome this inefficiency
a number of specialized non-CNF solvers were created. These
solvers were shown to have great advantages. Unfortunately,
non-CNF solvers cannot benefit from sophisticated CNF-based
techniques developed over the years.
This paper demonstrates how the power of non-CNF structure
can be harvested without the need for specialized solvers; in
fact, it is easily incorporated into most existing CNF-based QBF
solvers using a pre-existing mechanism of cube learning. We
demonstrate this using a state-of-the-art QBF solver DepQBF,
and experimentally show the effectiveness of our approach.