The Riis Complexity Gap for QBF Resolution

Beyersdorff, Olaf; Clymo, Judith; Dantchev, Stefan; Martin, Barnaby

Abstract

We give an analogue of the Riis Complexity Gap Theorem in Resolution for Quantified Boolean Formulas (QBFs). Every first-order sentence ϕ without finite models gives rise to a sequence of QBFs whose minimal refutations in tree-like QBF Resolution systems are either of polynomial size (if ϕ has no models) or at least exponential in size (if ϕ has some infinite model). However, we show that this gap theorem is sensitive to the translation and different translations are needed for different QBF resolution systems. For tree-like Q-Resolution, the translation to QBF must be given additional structure in order for the polynomial upper bound to hold. This extra structure is not needed in the system tree-like ∀Exp+Res, where we see the complexity gap on a natural translation to QBF.

Citation

Beyersdorff, O., Clymo, J., Dantchev, S., & Martin, B. (2024). The Riis Complexity Gap for QBF Resolution. Journal on Satisfiability, Boolean Modeling and Computation, 15(1), 9-25. https://doi.org/10.3233/sat-231505

• Journal Article Type: Article
• Acceptance Date: Oct 16, 2024
• Online Publication Date: Oct 29, 2024
• Publication Date: 2024
• Deposit Date: Nov 13, 2024
• Publicly Available Date: Nov 13, 2024
• Journal: Journal on Satisfiability, Boolean Modeling and Computation
• Print ISSN: 1574-0617
• Publisher: IOS Press
• Peer Reviewed: Peer Reviewed
• Volume: 15
• Issue: 1
• Pages: 9-25
• DOI: https://doi.org/10.3233/sat-231505
• Public URL: https://durham-repository.worktribe.com/output/3090404