An algorithm for solving the satisfiability problem is presented. It is proved that this algorithm solves 2-SAT and Horn-SAT in linear time and k-positive SAT (in which every clause contains at most k positive literals) in time O(|F|.ζ~n_k, where |F| is the length of input F, n is the number of atoms occurring in F, andζ_k, is the greatest real number satisfying the equation x = 2-1/x~k. Compared with previous x results, this nontrivial upper bound on time complexity could only be obtained for k-SAT, which is a subproblem of k-positive SAT.
展开▼
机译：提出了一种解决可满足性问题的算法。证明了该算法在线性时间和时间为O（| F |.ζ〜n_k，其中| F |的k个正SAT（每个子句最多包含k个正文字）中求解2-SAT和Horn-SAT。是输入F的长度，n是在F中出现的原子数，ζ_k是满足方程x = 2-1 / x〜k的最大实数，与先前的x结果相比，该非平凡的时间复杂度上限只能针对k-SAT获得，这是k正SAT的一个子问题。
展开▼
