QBF Merge Resolution 强大但不自然
QBF Merge Resolution is powerful but unnatural
AI总结：
本文比较 QBF 证明系统 M-Res 与 LD-Q-Res 等，证明其相对最强归结系统具有指数优势且二者不可比，并揭示其在限制下不封闭、配合弱化可获指数收益。
摘要：
Beyersdorff 等人于 2019 年提出的用于 QBF 的 Merge Resolution 证明系统（M-Res）在反驳中显式构建部分策略。这种方法最初的动机是克服长距离 Q-Resolution 证明系统（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 最好配合弱化使用，不过带弱化的 M-Res 是否在限制下封闭仍然是开放问题。我们指出，即使带有弱化，M-Res 仍继续可由 eFrege $+$ $\ orall$red 模拟（普通 M-Res 的模拟最近由 Chew 和 Slivovsky 给出）。
英文摘要：
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).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
