Hinweis
Dieser Eintrag wurde automatisch aus einem Altsystem migriert. Die Daten wurden nicht überprüft und entsprechen eventuell nicht den Qualitätskriterien des vorliegenden Systems.
E192-01 - Forschungsbereich Algorithms and Complexity
-
Zeitschrift:
Journal of Artificial Intelligence Research
-
ISSN:
1076-9757
-
Datum (veröffentlicht):
2019
-
Umfang:
28
-
Peer Reviewed:
Ja
-
Keywords:
Artificial Intelligence
-
Abstract:
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...
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.