Florian Lonsing, Armin Biere,
"Failed Literal Detection for QBF"
: Proc. 14th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'11), Serie Lecture Notes in Computer Science (LNCS), Vol. 6695, Springer, Seite(n) 259-272, 6-2011
Original Titel:
Failed Literal Detection for QBF
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 14th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'11)
Original Kurzfassung:
Failed literal detection (FL) in SAT is a powerful approach
for preprocessing. The basic idea is to assign a variable as assumption. If
boolean constraint propagation (BCP) yields an empty clause then the
negated assumption is necessary for satisfiability. Whereas FL is common
in SAT, it cannot easily be applied to QBF due to universal quantification.
We present two approaches for FL to preprocess prenex CNFs. The
first one is based on abstraction where certain universal variables are
treated as existentially quantified. Second we combine QBF-specific BCP
(QBCP) in FL with Q-resolution to validate assignments learnt by FL.
Finally we compare these two approaches to a third common approach
based on SAT. It turns out that the three approaches are incomparable.
Experimental evaluation demonstrates that FL for QBF can improve the
performance of search- and elimination-based QBF solvers.
Forschungs-