Failed Literal Detection for QBF

7 years 9 months ago
Failed Literal Detection for QBF
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 ne 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.
Florian Lonsing, Armin Biere
Added 17 Sep 2011
Updated 17 Sep 2011
Type Journal
Year 2011
Where SAT
Authors Florian Lonsing, Armin Biere
Comments (0)