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) MRes 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 MRes 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).
翻译:Beyersdorf等人于2019年提议的QBFF的合并分辨率校验系统(M-Res)在2019年Beyersdorff等人提出的对QBFF的合并分辨率校验系统(M-Res)在反驳中明确建立了部分战略。这种方法的最初动机是克服长距离Q分辨率校验系统(LD-Q-Res)(LD-Q分辨率校验系统(LD-Q-Res))(LD-Resdorf等人在2019年提出的合并分辨率校验系统(M-Res)中遇到的限制,同时禁止所有不健全的决议,最终也禁止了一些健全的决议。然而,虽然M-Reserf(M-Res-Res)比其他许多基于分辨率的Q-Reserf(Q-Res-Ref)验证系统的优势已经显现出来,与LQ-Res-Res-Reserf(LQ-Res-Res)本身的变现的变现能力相比,我们解决了这一问题。我们的证据方法显示M-Res-res的变弱程度是否比M-递增(MRes)系统更接近和变弱。我们的证据显示,我们使用的是一种不固定的变弱的变弱的系统。