Producing and verifying extremely large propositional refutations
Producing and verifying extremely large propositional refutations
复制标题
产生并验证极大的命题反驳
DOI：
10.1007/s10472-012-9322-x
复制
发表时间：
2012
影响因子：
1.2
通讯作者：
A. V. Gelder
中科院分区：
文献类型：
--
作者：
A. V. Gelder
对于高性能的命题可满足性求解器，产生不可满足性证书的重要性越来越被认识到。领先的求解器开发冲突图作为派生（或“学习”）新子句的基础。从冲突图中提取解决推导在理论上是简单的，但解决证明可能非常长。本文报告了一个工具，已验证证明超过1600千兆字节长。已经提出并研究了几种其他的证书格式，但是这些格式的验证器在其自身的权利中不可能实现自动验证。然而，一些替代格式享有的优点是容易产生的证据，并在其空间要求合理。本文报告了开发一个实用的系统，一个更紧凑的证书格式的正式验证的进展。实验比较。介绍了一种称为RUP（反向单元传播）的格式，并评估了两种实现。该方法是Goldberg和Novikov提出的冲突子句证明的推广，并且与冲突子句最小化兼容。简要讨论了从其它可判定理论中提取归结导数的问题。
The importance of producing a certificate of unsatisfiability is increasingly recognized for high performance propositional satisfiability solvers. The leading solvers develop a conflict graph as the basis for deriving (or “learning”) new clauses. Extracting a resolution derivation from the conflict graph is theoretically straightforward, but resolution proofs can be extremely long. This paper reports on a tool that has verified proofs more than 1600 gigabytes long. Several other certificate formats have been proposed and studied, but the verifiers for these formats are beyond any hope of automated verification in their own rights. However, some of the alternative formats enjoy the advantages of being easy to produce proofs for, and reasonable in their space requirements. This paper reports progress on developing a practical system for formal verification of a more compact certificate format. Experimental comparisons are presented. A format called RUP (for Reverse Unit Propagation) is introduced and two implementations are evaluated. This method is an extension of conflict-clause proofs introduced by Goldberg and Novikov, and is compatible with conflict-clause minimization. Extracting a resolution derivation from other decidable theories is discussed briefly.