Complexity of Finding Short Resolution Proofs
Complexity of Finding Short Resolution Proofs
复制标题
寻找短分辨率证明的复杂性
DOI：
10.1007/bfb0029974
复制
发表时间：
1997
影响因子：
0.6
通讯作者：
K. Iwama
中科院分区：
文献类型：
--
作者：
K. Iwama
本文讨论了n元CNF公式的最短分解证明问题。证明了：如果存在一个多项式时间(分别为超多项式时间或次指数时间)的近似算法，其长度可达S+O(n，d)，其中S是最短证明的长度，且d可以是任意常数，则存在一个多项式时间(分别为超多项式时间或次指数时间)的算法来解决(传统的)可满足性。这立即给出了一个公开问题的肯定答案，该问题询问寻找最短分解证明是否是NP难的。
This paper discusses the problem of finding a shortest Resolution proof for a CNF formula of n variables. It is shown that if there is a polynomial-time (superpolynomial-time or subexponential time, respectively) approximation algorithm that finds a nearly shortest proof of length up to S + O(n d ), where S is the length of the shortest proof and d may be any constant, then there is a polynomial-time (superpolynomial-time or subexponential-time, respectively) algorithm that solves the (conventional) satisfiability of CNF formulas. This immediately gives a positive answer to the open problem asking whether finding a shortest Resolution proof is NP-hard.