QCDCL with Cube Learning or Pure Literal Elimination - What Is Best?
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.
Cite
Text
Böhm et al. "QCDCL with Cube Learning or Pure Literal Elimination - What Is Best?." International Joint Conference on Artificial Intelligence, 2022. doi:10.24963/IJCAI.2022/248Markdown
[Böhm et al. "QCDCL with Cube Learning or Pure Literal Elimination - What Is Best?." International Joint Conference on Artificial Intelligence, 2022.](https://mlanthology.org/ijcai/2022/bohm2022ijcai-qcdcl/) doi:10.24963/IJCAI.2022/248BibTeX
@inproceedings{bohm2022ijcai-qcdcl,
title = {{QCDCL with Cube Learning or Pure Literal Elimination - What Is Best?}},
author = {Böhm, Benjamin and Peitl, Tomás and Beyersdorff, Olaf},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2022},
pages = {1781-1787},
doi = {10.24963/IJCAI.2022/248},
url = {https://mlanthology.org/ijcai/2022/bohm2022ijcai-qcdcl/}
}