Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking

技术摘要：基于纯路径的强 (D)QBF 依赖方案及其在证明检查中的应用

问题陈述
量化布尔公式（QBF）和依赖量化布尔公式（DQBF）的认证仍然是一个重大挑战。尽管近期的证明复杂度研究表明，“独立扩展”（IndExt）规则使得 IndExtQURes 证明系统能够 p-模拟绝大多数现有的 QBF 和 DQBF 技术，但 IndExtQURes 本身尚未成为一种实用的认证格式。相反，像 QRAT（量化非对称重言式）及其 DQBF 推广 DQRAT（依赖量化非对称重言式）这样的实用格式，缺乏 p-模拟 IndExtQURes 的理论强度。具体而言，依赖反射归约路径依赖方案（$D_{rrs}$）的 DQRAT，尚未被证明能达到 IndExtQURes 的强度，这在理论最优性与实用认证之间留下了空白。

方法论
作者通过引入一种名为 $D_{\forall pure}$（纯全称依赖方案）的新依赖方案来填补这一空白。该方案基于“纯路径”的概念，限制了全称文字与存在文字之间的归约路径。与标准的反射归约路径（$D_{rrs}$）不同，$D_{\forall pure}$ 会排除从全称文字 $u$ 到存在文字 $x$ 的归约路径，前提是该路径仅仅是从 $\bar{u}$ 到 $x$ 的路径的扩展。这确保了仅保留最小且必要的依赖关系。

方法论包含三个主要组成部分：

1. 定义与可靠性：作者利用子句集和文字的不动点构造，形式化地定义了 $D_{\forall pure}$。他们证明了该方案的语义可靠性（定理 10），表明移除由 $D_{\forall pure}$ 识别的虚假依赖关系不会改变 DQBF 的真值。
2. 集成到证明系统中：作者将 $D_{\forall pure}$ 集成到 DQRAT 证明系统中，创建了一个新系统，记为 DQRAT+$D_{\forall pure}$。他们还定义了一个局部归约规则 Loc$_{\forall pure}$-Red，该规则允许在不改变前缀的情况下直接归约包含全称文字的子句，前提是到冲突子句不存在纯路径。
3. 复杂度分析：本文建立了新系统与 IndExtQURes 之间的关系。作者证明了 DQRAT+$D_{\forall pure}$ 与 IndExtQURes 是 p-等价 的（多项式时间等价）。这是通过证明 DQRAT+$D_{\forall pure}$ 可以 p-模拟 IndExtQURes（即利用新依赖方案模拟独立扩展规则以移除不必要的依赖）以及 IndExtQURes 可以 p-模拟 DQRAT+$D_{\forall pure}$ 来实现的。

主要贡献

• 新依赖方案（$D_{\forall pure}$）：本文引入了一种依赖方案，在特定上下文中（例如，分离 LD-Q(Drrs)-Res 与 LD-Q(D$_{\forall pure}$)-Res）比 $D_{rrs}$ 严格更强，同时保持了多项式时间的可检查性。
• 证明系统等价性：主要的理论贡献是证明了 DQRAT+$D_{\forall pure}$ 与 IndExtQURes 是 p-等价的。这意味着 DQRAT+$D_{\forall pure}$ 可以 p-模拟 IndExtQURes 所能模拟的所有主要 QBF 和 DQBF 证明系统，包括 QRAT、G 以及各种依赖方案规则。
• 策略提取：作者表明 $D_{\forall pure}$ 是一种“正规”依赖方案，这使得在长距离 Q-归约（LD-Q-Res）中能够进行多项式时间的策略提取。这一结果支持将 $D_{\forall pure}$ 可靠地集成到如 Qute 等求解器中。
• 实现：作者实现了一个原型证明检查器 DQRAT-check，支持 DQRAT+$D_{\forall pure}$ 格式。他们还扩展了 Qute 求解器，以利用 $D_{\forall pure}$ 进行子句学习。

结果

• 理论方面：本文表明，$D_{\forall pure}$ 允许移除 $D_{rrs}$ 无法移除的依赖关系，特别是在涉及“桥接”奇偶公式的情况下，$D_{rrs}$ 未能检测到独立性，而 $D_{\forall pure}$ 则能成功检测。
• 实验方面（证明检查）：原型检查器在 QBFEval 2022 的基准测试和手工构造的公式（包括本文中的示例）上进行了测试。检查器成功验证了证明。作者指出，证明提取以及从 QRP（Qute 的内部格式）到 DQRAT 的转换占据了检查时间的 97%，而 DQRAT 检查器本身仅占 3%。
• 实验方面（求解）：当集成到 Qute 求解器中时，$D_{\forall pure}$ 在 QBFEval 2020 基准测试上显示出前景，将依赖计算时间减少了 7 倍，并且与 $D_{rrs}$ 相比发现了两倍多的独立对。然而，在更新的 QBFEval 2022 基准测试上，$D_{\forall pure}$ 未检测到新的独立性，且开销并未改善已解决实例的数量或 PAR2 分数。

意义
本文声称其主要意义在于弥合了理论证明强度与实用认证格式之间的差距。通过表明对现有 DQRAT 框架的简单修改（添加 $D_{\forall pure}$ 规则）即可产生一个与强大的 IndExtQURes p-等价的系统，作者为 QBF 和 DQBF 的统一、强认证标准提供了一条路径。这避免了需要针对 IndExtQURes 证明每个单独证明系统的 p-模拟，而是依赖于 DQRAT+$D_{\forall pure}$ 与 IndExtQURes 之间等价性的传递性。此外，这项工作提供了具体的实现（DQRAT-check），并展示了将这些强依赖方案集成到现有求解基础设施中的可行性，为未来 DQBF 求解器中更稳健的认证铺平了道路。