论文标题
QBF合并分辨率是强大但不自然的
QBF Merge Resolution is powerful but unnatural
论文作者
论文摘要
Beyersdorff等人提出的QBF的合并分辨率证明系统（M-RES）。在2019年，明确建立了驳斥内部的部分策略。这种方法的最初动机是克服在长距离Q分辨率证明系统（LD-Q-RES）中遇到的局限性，在该系统中，句法侧条条件同时禁止所有不符合的分辨率，最终也禁止某些合理的分辨率。但是，尽管已经证明了M-RES比许多其他基于决议的QBF证明系统的优势，但与LD-Q-RES本身的比较仍然开放。在本文中，我们解决了这个问题。我们表明，M-Res不仅比LD-Q-Res具有指数优势，而且在LQU $^+$ - RES和IRM上，这是当前已知的基于分辨率的QBF证明系统中最强大的功能。将其与Beyersdorff等人的结果相结合。 2020年，我们得出结论，M-Res与LQU-RES和LQU $^+$ - RES无与伦比。我们的证明方法揭示了有关M-RES的两个额外和好奇的特征：（i）M-RES在限制下未关闭，因此不是自然的证明系统，并且（ii）具有存在变量的公理条款削弱，证明可以在不弱化的情况下产生指数优势。我们进一步表明，在常规派生的背景下，用普遍变量削弱公理从句可以在不削弱的情况下获得指数优势。这些结果表明，M-RES可以更好地用于削弱，尽管在限制下关闭的M-RES是否在限制下关闭。我们注意到，即使随着弱点的变化，M-RES仍会继续由Efrege $+$ $ $ \ forall $ RED模拟（Chew and Slivovsky最近显示了普通M-Res的模拟）。
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).
