Separating signs in the propositional satisfiability problem

被引：0

作者：

Hirsch E.A.

机构：

来源：

Journal of Mathematical Sciences | 2000年 / 98卷 / 4期

关键词：

Sign Separation; Propositional Formula; Satisfiability Problem; Separation Principle; Propositional Satisfiability;

D O I：

10.1007/BF02362266

中图分类号：

学科分类号：

摘要：

In 1980, Monien and Speckenmeyer and (independently) Dantsin proved that the satisfiability of a propositional formula in CNF can be checked in less than 2N steps (N is the number of variables). Later, many other upper bounds for SAT and its subproblems were proved. A formula in CNF is in CNF- (1, ∞) if each positive literal occurs in it at most once. In 1984, Luckhardt studied formulas in CNF-(1, ∞). In this paper, we prove several a new upper bounds for formulas in CNF-(l.∞) by introducing new signs separation principle. Namely, we present algorithms working in time of order 1.1939K and 1.0644L for a formula consisting of K clauses containing L literal occurrences. We also present an algorithm for formulas in CNF-(1, ∞) whose clauses are bounded in length. © 2000 Kluwer Academic/Plenum Publishers.

引用

页码：442 / 463

页数：21

共 14 条

[1]

Garey M.R., Johnson D.S., Computers and Intractability. A Guide to the Theory of NP-completeness, (1979)

[2]

Dantsin E., Tautology Proof Systems Based on the Splitting Method, (1983)

[3]

Dantsin E., The algorithmics of the prepositional satisfiability problem, Problems of Reducing the Exhaustive Search, 178, (1997)

[4]

Dantsin E., Kreinovich V., Exponential upper bounds for the prepositional satisfiability problem, Proceedings of the 9th National Conference on Mathematical Logic, (1988)

[5]

Davis M., Putnam H., A computing procedure for quantification theory, J. Assoc. Comp. Mach., 7, pp. 201-215, (1960)

[6]

Hirsch E.A., Deciding satisfiability of formulas with K clauses in less than 2<sup>0. 30897k</sup>steps, POMI Preprint, (1997)

[7]

Hirsch E.A., Two new upper bounds for SAT, Proceedings of the Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 521-530, (1998)

[8]

Kullmann O., A systematical approach to 3 SAT-decision, yielding 3-SAT-decision in less than 1.5045<sup>n</sup> steps, Theoretical Computer Science

[9]

Kullmann O., Worst-case analysis, 3-SAT decision and lower bounds: Approaches for improved SAT algorithms, DIMACS Proceedings SAT Workshop 1996, (1996)

[10]

Kullmann O., Luckhardt H., Deciding prepositional tautologies: Algorithms and their complexity, Information and Computation, (1997)

← 1 2 →