Strong Extension-Free Proof Systems
Strong Extension-Free Proof Systems
复制标题
DOI：
10.1007/s10817-019-09516-0
复制
发表时间：
2020-03-01
期刊：
影响因子：
--
通讯作者：
Biere, Armin
中科院分区：
文献类型：
--
作者：
Heule, Marijn J. H.;Kiesl, Benjamin;Biere, Armin
我们介绍命题逻辑的证明系统，承认短证明的硬公式，以及现代SAT求解器使用的大多数技术的简洁表达。我们的证明系统允许派生的条款，不一定是隐含的，但这是多余的，在这个意义上说，他们的加法保持可满足性。为了保证这些增加的条款是冗余的，我们考虑各种有效的可判定的冗余标准，我们得到的第一个特征条款冗余的语义蕴涵关系，然后限制这种关系，使其成为可判定的多项式时间。由于限制蕴涵关系是基于单位传播-SAT求解器的核心技术-它也允许有效的证明检查。由此产生的证明系统是令人惊讶的强大，即使没有引入新的变量-证明复杂性文献中提出的简短证明的一个关键特征。我们证明了我们的证明系统的实力，著名的鸽子洞公式提供短子句证明没有新的变量。
We introduce proof systems for propositional logic that admit short proofs of hard formulas as well as the succinct expression of most techniques used by modern SAT solvers. Our proof systems allow the derivation of clauses that are not necessarily implied, but which are redundant in the sense that their addition preserves satisfiability. To guarantee that these added clauses are redundant, we consider various efficiently decidable redundancy criteria which we obtain by first characterizing clause redundancy in terms of a semantic implication relationship and then restricting this relationship so that it becomes decidable in polynomial time. As the restricted implication relation is based on unit propagation-a core technique of SAT solvers-it allows efficient proof checking too. The resulting proof systems are surprisingly strong, even without the introduction of new variables-a key feature of short proofs presented in the proof-complexity literature. We demonstrate the strength of our proof systems on the famous pigeon hole formulas by providing short clausal proofs without new variables.