QCDCL with Cube Learning or Pure Literal Elimination - What is Best?

QCDCL with Cube Learning or Pure Literal Elimination - What is Best?

Benjamin Böhm, Tomáš Peitl, Olaf Beyersdorff

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence
Main Track. Pages 1781-1787. https://doi.org/10.24963/ijcai.2022/248

Quantified conflict-driven clause learning (QCDCL) is one of the main approaches for solving quantified Boolean formulas (QBF). We formalise and investigate several versions of QCDCL that include cube learning and/or pure-literal elimination, and formally compare the resulting solving models via proof complexity techniques. Our results show that almost all of the QCDCL models are exponentially incomparable with respect to proof size (and hence solver running time), pointing towards different orthogonal ways how to practically implement QCDCL.
Keywords:
Constraint Satisfaction and Optimization: Satisfiabilty
Constraint Satisfaction and Optimization: Solvers and Tools