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

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

IJCAI 2022poster6 citations

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

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

Abstract

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.

Constraint Satisfaction and Optimization: SatisfiabiltyConstraint Satisfaction and Optimization: Solvers and Tools

BibTeX

@inproceedings{ijcai2022p248,
  title     = {QCDCL with Cube Learning or Pure Literal Elimination - What is Best?},
  author    = {Böhm, Benjamin and Peitl, Tomáš and Beyersdorff, Olaf},
  booktitle = {Proceedings of the Thirty-First International Joint Conference on
               Artificial Intelligence, {IJCAI-22}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Lud De Raedt},
  pages     = {1781--1787},
  year      = {2022},
  month     = {7},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2022/248},
  url       = {https://doi.org/10.24963/ijcai.2022/248},
}