Meena Mahajan ; Gaurav Sood - QBF Merge Resolution is powerful but unnatural

lmcs:12710 - Logical Methods in Computer Science, September 10, 2024, Volume 20, Issue 3 - https://doi.org/10.46298/lmcs-20(3:22)2024
QBF Merge Resolution is powerful but unnaturalArticle

Authors: Meena Mahajan ; Gaurav Sood

    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 incomparable with LQU-Res and LQU$^+$-Res. Our proof method reveals two additional and curious features about M-Res: (i) M-Res is not closed under restrictions, and is hence not a natural proof system, and (ii) weakening axiom clauses with existential variables provably yields an exponential advantage over M-Res without weakening. We further show that in the context of regular derivations, weakening axiom clauses with universal variables provably yields an exponential advantage over M-Res without weakening. These results suggest that M-Res is better used with weakening, though whether M-Res with weakening is closed under restrictions remains open. We note that even with weakening, M-Res continues to be simulated by eFrege $+$ $\forall$red (the simulation of ordinary M-Res was shown recently by Chew and Slivovsky).


    Volume: Volume 20, Issue 3
    Published on: September 10, 2024
    Accepted on: July 22, 2024
    Submitted on: December 19, 2023
    Keywords: Computer Science - Computational Complexity,Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 588 times.
    This article's PDF has been downloaded 226 times.