项消解的阿喀琉斯之踵
计算机科学中的逻辑
2017-04-05 v1
摘要
项消解提供了一种优雅的机制来证明量词布尔公式（QBF）为真。它是Q消解（也称为子句消解）的对偶，并且在实际中非常重要，因为它能够为基于DPLL的QBF求解器的答案提供证书。虽然项消解和Q消解非常相似，但它们并不完全对称。具体而言，Q消解作用于子句，而项消解作用于矩阵的模型。本文研究了这种不对称性产生的影响。我们将看到存在一大类公式（具有“大模型”的公式），其项消解证明是指数级的。作为一种可能的补救措施，本文建议通过反驳其否定（negate-refute）来证明QBF为真，而不是通过项消解来证明它们。本文表明，从理论角度来看，这确实是一种有利的方法。具体而言，否定-反驳可以p-模拟项消解，并且两种演算之间存在指数级分离。这些观察结果加深了我们对QBF证明系统的理解，并为非CNF QBF求解器的努力提供了坚实的理论基础。
关键词
引用
@article{arxiv.1704.01071,
title = {An Achilles' Heel of Term-Resolution},
author = {Mikoláš Janota},
journal= {arXiv preprint arXiv:1704.01071},
year = {2017}
}