Armin Biere, Florian Lonsing, Martina Seidl,
"Blocked Clause Elimination for QBF"
: Proc. 23rd Intl. Conf. on Automated Deduction (CADE'11), Serie Lecture Notes in Computer Science (LNCS), Vol. 6803, Springer, Seite(n) 101-115, 8-2011
Blocked Clause Elimination for QBF
Sprache des Titels:
Proc. 23rd Intl. Conf. on Automated Deduction (CADE'11)
Quantified Boolean formulas (QBF) provide a powerful framework
for encoding problems from various application domains, not least
because efficient QBF solvers are available. Despite sophisticated evaluation
techniques, the performance of such a solver usually depends on the
way a problem is represented. However, the translation to processable
QBF encodings is in general not unique and may either introduce variables
and clauses not relevant for the solving process or blur information
which could be beneficial for the solving process. To deal with both of
these issues, preprocessors have been introduced which rewrite a given
QBF before it is passed to a solver.
In this paper, we present novel preprocessing methods for QBF based
on blocked clause elimination (BCE), a technique successfully applied in
SAT. Quantified blocked clause elimination (QBCE) allows to simulate
various structural preprocessing techniques as BCE in SAT. We have implemented
QBCE and extensions of QBCE in the preprocessor bloqqer.
In our experiments we show that preprocessing with QBCE reduces formulas
substantially and allows us to solve considerable more instances
than the previous state-of-the-art.