Dynamic Dependency Awareness for QBF

Dynamic Dependency Awareness for QBF

Joshua Blinkhorn, Olaf Beyersdorff

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence
Best Sister Conferences. Pages 5224-5228. https://doi.org/10.24963/ijcai.2018/726

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.
Keywords:
Knowledge Representation and Reasoning: Automated Reasoning and Theorem Proving