QBF 合并归结功能强大但不自然
计算复杂性
2024-09-11 v5 计算机科学中的逻辑
摘要
Beyersdorff 等人于 2019 年提出的针对 QBF 的合并归结证明系统（M-Res）在反驳中显式构建部分策略。该方法最初的动机是克服长距离 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 最好与弱化一起使用，尽管带弱化的 M-Res 是否在限制下封闭仍属开放问题。我们注意到，即使带弱化，M-Res 仍继续被 eFrege red 模拟（普通 M-Res 的模拟最近由 Chew 和 Slivovsky 给出）。
引用
@article{arxiv.2205.13428,
title = {QBF Merge Resolution is powerful but unnatural},
author = {Meena Mahajan and Gaurav Sood},
journal= {arXiv preprint arXiv:2205.13428},
year = {2024}
}