The complexity of satisfiability problems

ABSTRACT

The problem of deciding whether a given propositional formula in conjunctive normal form is satisfiable has been widely studied. I t is known that, when restricted to formulas having only two literals per clause, this problem has an efficient (polynomial-time) solution. But the same problem on formulas having three literals per clause is NP-complete, and hence probably does not have any efficient solution. In this paper, we consider an infinite class of satisfiability problems which contains these two particular problems as special cases, and show that every member of this class is either polynomial-time decidable or NP-complete. The infinite collection of new NP-complete problems so obtained may prove very useful in finding other new NP-complete problems. The classification of the polynomial-time decidable cases yields new problems that are complete in polynomial time and in nondeterministic log space. We also consider an analogous class of problems, involving quantified formulas, which has the property that every member is either polynomial time decidable or complete in polynomial space.

REFERENCES

• 1: M. Bauer, D. Brand, M. Fischer, A. Meyer and M. Paterson, A note on disjunctive form tautologies, SIGACT News April 1973, pp. 17-20.
• 2: Stephen A. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing, p.151-158, May 03-05, 1971, Shaker Heights, Ohio, United States [doi>10.1145/800157.805047]
• 3: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 4: N.D. Jones, Space-bounded reducibility among combinatorial problems, J. Comp. Sys. Sci. 11 (1975) pp. 68-85.
• 5: Neil D. Jones , William T. Laaser, Complete problems for deterministic polynomial time, Proceedings of the sixth annual ACM symposium on Theory of computing, p.40-46, April 30-May 02, 1974, Seattle, Washington, United States [doi>10.1145/800119.803883]
• 6: R.M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, R.W. Miller and J.W. Thatcher eds., Plenum Press, New York, 1972, pp. 85-104.
• 7: E.L. Post, The two-valued iterative systems of mathematical logic, Annals of Math. Studies, vol. 5, Princeton, 1941.
• 8: W. Savitch, Relationships between nondetermin-istic and deterministic tape complexities, J. Comp. Sys. Sci. 4 (1970), pp. 177-192.
• 9: Thomas J. Schaefer, Complexity of decision problems based on finite two-person perfect-information games, Proceedings of the eighth annual ACM symposium on Theory of computing, p.41-49, May 03-05, 1976, Hershey, Pennsylvania, United States [doi>10.1145/800113.803629]
• 10: L.J. Stockmeyer, The polynomial-time hierarchy, Theor. Comp. Sci. 3 (1976), pp. 1-22.
• 11: L. J. Stockmeyer , A. R. Meyer, Word problems requiring exponential time(Preliminary Report), Proceedings of the fifth annual ACM symposium on Theory of computing, p.1-9, April 30-May 02, 1973, Austin, Texas, United States [doi>10.1145/800125.804029]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness

General Terms:
Algorithms, Theory