理解QBF CDCL求解器与QBF消解的相对强度

实现QCDCL范式的QBF求解器是功能强大的算法，能够成功应对许多计算复杂的应用。然而，我们对这些QCDCL求解器的强度与局限性的理论理解非常有限。在本文中，我们建议将QCDCL求解器形式化建模为证明系统。我们定义了可用于决策启发式和单元传播的不同策略，并由此产生若干可靠且完备的QBF证明系统（进而产生新的QCDCL算法）。对于实际QCDCL求解中使用的标准策略，我们证明相应的QCDCL证明系统与文献中使用的经典QBF消解系统Q-resolution不可比较（通过指数级分离）。这与命题逻辑设定形成鲜明对比，在命题逻辑中CDCL与消解已知是p等价的。这引出了一个问题：哪些公式对标准QCDCL是困难的，因为正如我们在此所示，Q-resolution下界并不必然适用于QCDCL。作为对该问题的回答，我们证明了QCDCL的若干下界，包括一大类随机QBF的指数级下界。我们还引入了对经典QCDCL中决策启发式的强化，该强化不一定按前缀顺序决定变量，但仍允许学习断言子句。我们证明，采用该决策策略时，QCDCL在某些公式上可以快指数倍。我们进一步展示了一个与Q-resolution p等价的QCDCL证明系统。与经典QCDCL相比，这一新版本的QCDCL同时调整了决策和单元传播策略。