Heule Marijn J H, Kiesl Benjamin, Biere Armin
1Department of Computer Science, The University of Texas, Austin, USA.
2Institute of Logic and Computation, TU Wien, Vienna, Austria.
J Autom Reason. 2020;64(3):533-554. doi: 10.1007/s10817-019-09516-0. Epub 2019 Feb 22.
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.
我们引入了用于命题逻辑的证明系统，该系统允许对难题公式进行简短证明，同时也能简洁地表达现代SAT求解器所使用的大多数技术。我们的证明系统允许推导不一定被蕴含但在添加后保持可满足性意义上是冗余的子句。为了确保这些添加的子句是冗余的，我们考虑了各种可有效判定的冗余标准，这些标准是通过首先根据语义蕴含关系来刻画子句冗余，然后对这种关系进行限制，使其在多项式时间内可判定而得到的。由于受限的蕴含关系基于SAT求解器的核心技术——单元传播，它也允许进行高效的证明检查。即使不引入新变量（这是证明复杂性文献中简短证明的一个关键特征），由此产生的证明系统也出奇地强大。我们通过提供无新变量的简短子句证明，展示了我们的证明系统在著名的鸽巢公式上的强大之处。
