Solving satisfiability in less than 2n steps
作者： B. Monien , E. Speckenmeyer
DOI: 10.1016/0166-218X(85)90050-2
关键词:
摘要: In this paper we describe and analyse an algorithm for solving the satisfiability problem. If E is a boolean formula in conjunctive normal form with n variables r clauses, then will show that solves problem formulas at most k literals per clause time O(|F|.@a"k^n), where @a"k greatest number satisfying = 2-1/@a"k^k^-^1 (in case of 3-satisfiability @a"3 1,6181).
acm.org
elsevier.com
sci-hub.se 参考文章(3)
Allen Goldberg, Paul Purdom, Cynthia Brown, Average time analysis of simplified Davis-Putnam procedures Information Processing Letters. ,vol. 15, pp. 72- 75 ,(1982) , 10.1016/0020-0190(82)90110-7
John Franco, Marvin Paull, Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem Discrete Applied Mathematics. ,vol. 5, pp. 77- 87 ,(1983) , 10.1016/0166-218X(83)90017-3
Stephen A. Cook, The complexity of theorem-proving procedures symposium on the theory of computing. pp. 151- 158 ,(1971) , 10.1145/800157.805047