QCDCL vs QBF Resolution: Further Insights
Abstract
We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants – parameterised by different policies for decisions, unit propagations and reductions – lead to incomparable systems for almost all choices of these policies.
Cite
Text
Böhm and Beyersdorff. "QCDCL vs QBF Resolution: Further Insights." Journal of Artificial Intelligence Research, 2024. doi:10.1613/JAIR.1.15522Markdown
[Böhm and Beyersdorff. "QCDCL vs QBF Resolution: Further Insights." Journal of Artificial Intelligence Research, 2024.](https://mlanthology.org/jair/2024/bohm2024jair-qcdcl/) doi:10.1613/JAIR.1.15522BibTeX
@article{bohm2024jair-qcdcl,
title = {{QCDCL vs QBF Resolution: Further Insights}},
author = {Böhm, Benjamin and Beyersdorff, Olaf},
journal = {Journal of Artificial Intelligence Research},
year = {2024},
pages = {741-769},
doi = {10.1613/JAIR.1.15522},
volume = {81},
url = {https://mlanthology.org/jair/2024/bohm2024jair-qcdcl/}
}