二维学习与QCDCL证明系统中依赖方案的相互作用

量化冲突驱动子句学习（QCDCL）是求解量化布尔公式（QBF）的主要方法之一。二维学习用于确保可以验证真公式。依赖方案有助于检测由QBF量化前缀中变量排序所暗示但不用于构造（反）模型的伪依赖。这种检测可在特定证明系统中可证明地缩短归谬证据，预期可加速QBF求解器的运行。最简单的底层证明系统[ BeyersdorffB"ohm-LMCS2023]，在不使用二维学习也不使用依赖方案的情况下，对假公式的QCDCL方法进行形式化推理。[B"ohmPeitlBeyersdorff-AI2024]的工作进一步包含二维学习。[ChoudhuryMahajan-JAR2024]的工作包含有限使用的依赖方案，但不包含二维学习。在本文中，形式化了使用二维学习且在所有阶段都使用依赖方案的QCDCL求解器所基于的证明系统。提出了健全性和完备性的充分条件，证明使用标准和反射解析路径依赖方案（$D^{std}$ 和 $D^{rrs}$）以放宽决策顺序可证明地缩短归谬。当决策受限于遵循量化顺序，但在传播和学习中使用依赖方案并结合二维学习时，详细研究了使用依赖方案 $D^{std}$ 和 $D^{rrs}$ 的结果证明系统并分析了其相对优势。