<div class="csl-bib-body">
<div class="csl-entry">Böhm, B., Peitl, T., & Beyersdorff, O. (2024). QCDCL with cube learning or pure literal elimination – What is best? <i>Artificial Intelligence</i>, <i>336</i>, Article 104194. https://doi.org/10.1016/j.artint.2024.104194</div>
</div>
-
dc.identifier.issn
0004-3702
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/208031
-
dc.description.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 variants via proof complexity techniques. Our results show that almost all of the QCDCL variants are exponentially incomparable with respect to proof size (and hence solver running time), pointing towards different orthogonal ways how to practically implement QCDCL.
en
dc.language.iso
en
-
dc.publisher
ELSEVIER
-
dc.relation.ispartof
Artificial Intelligence
-
dc.rights.uri
https://creativecommons.org/licenses/by-nc/4.0/
-
dc.subject
Lower bounds
en
dc.subject
Proof complexity
en
dc.subject
QBF proof systems
en
dc.subject
Quantified Boolean formulas
en
dc.subject
Resolution
en
dc.subject
SAT solving
en
dc.title
QCDCL with cube learning or pure literal elimination – What is best?
en
dc.type
Article
en
dc.type
Artikel
de
dc.rights.license
Creative Commons Namensnennung - Nicht kommerziell 4.0 International
de
dc.rights.license
Creative Commons Attribution-NonCommercial 4.0 International