Submitter: Florian Lonsing
Description: Devised by Florian Lonsing, is a search-based solver with conflict-driven clause and solution-driven cube learning (QCDCL). The submitted variants of depqbf are based on version 5.0, with an advanced technique for cube learning by tightly integrating blocked clause elimination into QCDCL.
Details are available in
Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Logic for Programming, Artificial Intelligence, and Reasoning, Springer (2015) 418433
The submitted variants of depqbf, namely depqbf-v1, depqbf-v2, and depqbf-v3, extend version 5.0 by additionally integrating the SAT solver PicoSAT and the QBF preprocessor BLOQQER. PicoSAT and BLOQQER are applied dynamically during the run of QCDCL to derive clauses and cubes. This approach is described in
Lonsing, Florian, Uwe Egly, and Martina Seidl. "Q-Resolution with Generalized Axioms." International Conference on Theory and Applications of Satisfiability Testing. Springer International Publishing, 2016.
Additionally, DepQBF is combined with the preprocessors QxBF and BLOQQER in shellscripts.