[Back]

T. Peitl, F. Slivovsky, S. Szeider:
"Combining Resolution-Path Dependencies with Dependency Learning";
Talk: Int. Conference on Theory and Applications of Satisfiability Testing, Lissabon; 2019-07-07 - 2019-07-12; in: "Theory and Applications of Satisfiability Testing - SAT 2019", LNCS, 11628 (2019), ISBN: 978-3-030-24257-2; 306 - 318.

We present the first practical implementation of the reflexive
resolution-path dependency scheme in a QBF solver. Unlike in DepQBF,
which uses the less general standard dependency scheme, we do not compute
the dependency relation upfront, but instead query relevant dependencies
on demand during dependency conflicts, when the solver is about
to learn a missing dependency. Thus, our approach is fundamentally tied
to dependency learning, and shows that the two techniques for dependency
analysis can be fruitfully combined. As a byproduct, we propose a
quasilinear-time algorithm to compute all resolution-path dependencies
of a given variable. Experimental results on the QBF library confirm
the viability of our technique and identify families of formulas where the
speedup is particularly promising.

http://dx.doi.org/10.1007/978-3-030-24258-9

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