[Zurück]

T. Peitl, F. Slivovsky, S. Szeider:
"Dependency Learning for QBF";
Journal of Artificial Intelligence Research, 65 (2019), 65; S. 181 - 208.

Quantified Boolean Formulas (QBFs) can be used to succinctly encode problems from
domains such as formal verification, planning, and synthesis. One of the main approaches to
QBF solving is Quantified Con
ict Driven Clause Learning (QCDCL). By default, QCDCL
assigns variables in the order of their appearance in the quantifier prefix so as to account
for dependencies among variables. Dependency schemes can be used to relax this restriction
and exploit independence among variables in certain cases, but only at the cost of
nontrivial interferences with the proof system underlying QCDCL. We introduce depen-
dency learning, a new technique for exploiting variable independence within QCDCL that
allows solvers to learn variable dependencies on the
y. The resulting version of QCDCL
enjoys improved propagation and increased
exibility in choosing variables for branching
while retaining ordinary (long-distance) Q-resolution as its underlying proof system. We
show that dependency learning can achieve exponential speedups over ordinary QCDCL.
Experiments on standard benchmark sets demonstrate the effectiveness of this technique.

http://dx.doi.org/10.1613/jair.1.11529

https://publik.tuwien.ac.at/files/publik_282809.pdf