QBF Merge Resolution is powerful but unnatural
Meena Mahajan, Gaurav Sood

TL;DR
This paper demonstrates that Merge Resolution (M-Res) for QBFs is exponentially more powerful than several other resolution systems but is considered unnatural due to its lack of closure under restrictions and the benefits of weakening.
Contribution
The paper establishes the exponential separation of M-Res from other QBF proof systems and reveals its non-closure under restrictions and the advantages of weakening in proof complexity.
Findings
M-Res has exponential advantage over LD-Q-Res, LQU$^+$-Res, and IRM.
M-Res is incomparable with LQU-Res and LQU$^+$-Res.
Weakening with existential variables yields exponential advantage over M-Res.
Abstract
The Merge Resolution proof system (M-Res) for QBFs, proposed by Beyersdorff et al. in 2019, explicitly builds partial strategies inside refutations. The original motivation for this approach was to overcome the limitations encountered in long-distance Q-Resolution proof system (LD-Q-Res), where the syntactic side-conditions, while prohibiting all unsound resolutions, also end up prohibiting some sound resolutions. However, while the advantage of M-Res over many other resolution-based QBF proof systems was already demonstrated, a comparison with LD-Q-Res itself had remained open. In this paper, we settle this question. We show that M-Res has an exponential advantage over not only LD-Q-Res, but even over LQU-Res and IRM, the most powerful among currently known resolution-based QBF proof systems. Combining this with results from Beyersdorff et al. 2020, we conclude that M-Res is…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
