[Back]

F. Lonsing, U. Egly, A. Van Gelder:
"Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation";
Talk: 16th International Conference on Theory and Applications of Satisfiability Testing, Helsinki; 2013-07-08 - 2013-07-12; in: "Lecture Notes in Computer Science", (2013), ISBN: 978-3-642-39070-8; 100 - 115.

Recent solvers for quantified boolean formulas use a clause learning
method based on a procedure proposed by Giunchiglia et al. (JAIR 2006),
which avoids creating tautological clauses.
Recently, an exponential worst case for this procedure has been shown
by Van Gelder (CP 2012).
That paper introduced QBF Pseudo Unit Propagation (QPUP) for
non-tautological clause learning in a limited setting and showed that
its worst case is theoretically polynomial, although it might be impractical
in a high-performance QBF solver, due to excessive time and space
consumption. No implementation was reported.

This paper describes an enhanced version of QPUP clause learning that
is practical to incorporate into high-performance QBF solvers.
It can be used for proving that a QBF formula is either unsatisfiable
or satisfiable (working on both proofs in tandem),
and is compatible with pure-literal rules and dependency schemes.
A lazy version of QPUP permits non-tautological clauses to be learned
without actually carrying out resolutions, but this version is
unable to produce precise proofs.

Experimental results show that QPUP is somewhat faster than the
previous non-tautological clause learning procedure on benchmarks
from QBFEVAL-10.

QBF, clause learning, satisfiability

http://dx.doi.org/10.1007/978-3-642-39071-5_9