Dynamic Dependency Awareness for QBF
Abstract
We provide the first proof complexity results for QBF dependency calculi. By showing that the reflexive resolution path dependency scheme admits exponentially shorter Q-resolution proofs on a known family of instances, we answer a question first posed by Slivovsky and Szeider (SAT 2014). Further, we introduce a new calculus in which a dependency scheme is applied dynamically. We demonstrate the further potential of this approach beyond that of the existing static system with an exponential separation.
Cite
Text
Blinkhorn and Beyersdorff. "Dynamic Dependency Awareness for QBF." International Joint Conference on Artificial Intelligence, 2018. doi:10.24963/IJCAI.2018/726Markdown
[Blinkhorn and Beyersdorff. "Dynamic Dependency Awareness for QBF." International Joint Conference on Artificial Intelligence, 2018.](https://mlanthology.org/ijcai/2018/blinkhorn2018ijcai-dynamic/) doi:10.24963/IJCAI.2018/726BibTeX
@inproceedings{blinkhorn2018ijcai-dynamic,
title = {{Dynamic Dependency Awareness for QBF}},
author = {Blinkhorn, Joshua and Beyersdorff, Olaf},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2018},
pages = {5224-5228},
doi = {10.24963/IJCAI.2018/726},
url = {https://mlanthology.org/ijcai/2018/blinkhorn2018ijcai-dynamic/}
}