TY - GEN
T1 - Failed Literal Detection for QBF
AU - Lonsing, Florian
AU - Biere, Armin
PY - 2011/6
Y1 - 2011/6
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/79959393384
U2 - 10.1007/978-3-642-21581-0_21
DO - 10.1007/978-3-642-21581-0_21
M3 - Conference proceedings
SN - 9783642215803
VL - 6695
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 259
EP - 272
BT - Proc. 14th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'11)
PB - Springer
ER -