ECCC-Report TR21-131https://eccc.weizmann.ac.il/report/2021/131Comments and Revisions published for TR21-131en-usThu, 14 Jul 2022 17:48:01 +0300
Revision 1
| QCDCL with Cube Learning or Pure Literal Elimination - What is best? |
Benjamin Böhm,
Tomáš Peitl,
Olaf Beyersdorff
https://eccc.weizmann.ac.il/report/2021/131#revision1Quantified 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.Thu, 14 Jul 2022 17:48:01 +0300https://eccc.weizmann.ac.il/report/2021/131#revision1
Paper TR21-131
| QCDCL with Cube Learning or Pure Literal Elimination - What is best? |
Benjamin Böhm,
Olaf Beyersdorff
https://eccc.weizmann.ac.il/report/2021/131Quantified 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.Fri, 10 Sep 2021 20:29:36 +0300https://eccc.weizmann.ac.il/report/2021/131