Skip to main content
SpringerLink
Log in

Polynomial restrictions of SAT: What can be done with an efficient implementation of the Davis and Putnam's procedure?

  • Operation Research
  • Conference paper
  • First Online:
Book cover Principles and Practice of Constraint Programming — CP '95 (CP 1995)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 976))

Abstract

Constraint Solving Problems are NP-Complete and thus computationaly intractable. Two approaches have been used to tackle this intractability: the improvement of general purpose solvers and the research of polynomial time restrictions. An interesting question follows: what is the behavior of the former solvers on the latter restrictions?

In this paper, we examplify this problem by studying both theoretical and practical complexities of the Davis and Putnam's procedure on the two main polynomial restrictions of SAT, namely Horn-SAT and 2-SAT. We propose an efficient implementation and an improvement that make it quadratic in the worst case on these sub-classes. We show that this complexity is never reached in practice where linear times are observed, making the Davis and Putnam's as efficient as specialized algorithms.

This work is supported by the french inter-PRC project “Classes Polynomiales”

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. V. Arvind and S. Biswas. An O(n2) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes horn sentences. Information Processing Letters, 24:67–69, 1987.

    Article  Google Scholar 

  2. B. Aspvall. Recognizing Disguised NR(1) Instances of the Satisfiability Problem. Journal of Algorithms, 1:97–103, 1980.

    Article  Google Scholar 

  3. B. Aspvall, M. Plass, and R. Tarjan. A Linear Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulae. Information Processing Letter, 8(3):121–123, 1979.

    Article  Google Scholar 

  4. G. Ausiello and G. Italiano. On-Line Algorithms for Polynoinially Solvable Satisfiability Problems. Journal of Logic Programming, 10:69–90, 1990.

    Article  Google Scholar 

  5. A. Blass and Y. Gurevitch. On the unique satisfiability problem. Information and Control, 55:80–88, 1982.

    Article  Google Scholar 

  6. J.M. Boï and A. Rauzy. Two algorithms for constraints system solving in propositional calculus and their implementation in prologIII. In P. Jorrand and V. Sugrev, editors, Proceedings Artificial Intelligence IV Methodology, Systems, Applications (AIMSA'90), pages 139–148. North-Holand, September 1990. Alba-Varna bulgarie.

    Google Scholar 

  7. E. Boros, Y. Crama, and P.L. Hammer. Polynomial-time inference of all implications for Horn and related formulae. Annals of Mathematics and Artificial Intelligence, 1:21–32, 1990.

    Article  Google Scholar 

  8. E. Boros, Y. Crama, P.L. Hammer, and M. Saks. A complexity index for satisfiability problems. SIAM Journ. Comp., 23:45–49, 1994.

    Article  Google Scholar 

  9. E. Boros, P.L. Hammer, and X. Sun. Recognition of q-Horn formulae in linear time. Discrete Applied Mathematics, 55:1–13, 1994.

    Article  Google Scholar 

  10. V. Chandru, C.R. Coulard, P.L. Hammer, M. Montanez, and X. Sun. On renamable Horn and generalized Horn functions. In Annals of Mathematics and Artificial Intelligence, volume 1. J.C. Baltzer AG, Scientific Publishing Company, Basel Switzerland, 1990.

    Google Scholar 

  11. P. Cheeseman, B. Kanefsky, and W.M. Taylor. Where the Really Hard Problems Are. In Proceedings of the International Joint Conference of Artificial Intelligence, IJCAI'91, 1991.

    Google Scholar 

  12. V. Chvátal and B. Reed. Miks gets some (the odds are on his side). In Proceedings of the 33rd IEEE Symp. on Foundations of Computer Science, pages 620–627, 1992.

    Google Scholar 

  13. S.A. Cook. The Complexity of Theorem Proving Procedures. In Proceedings of the 3rd Ann. Symp. on Theory of Computing, ACM, pages 151–158, 1971.

    Google Scholar 

  14. M.C. Cooper, D.A. Cohen, and P.G. Jeavons. Characterizing Tractable Constraints. Artificial Intelligence, 65:347–361, 1994.

    Article  Google Scholar 

  15. J.M. Crawford and L.D. Anton. Experimental results on the crossover point in satisfiability problems. In Proceedings of the Eleventh National Conference on Artificial Intelligence (Washington, D.C., AAAI'1993), pages 21–27, 1993.

    Google Scholar 

  16. M. Davis, G. Logemann, and D. Loveland. A Machine Program for Theorem Proving. JACM, 5:394–397, 1962.

    Google Scholar 

  17. M. Davis and H. Putnam. A Computing Procedure for Quantification Theory. JACM, 7:201–215, 1960.

    Article  Google Scholar 

  18. W.F. Dowling and J.H. Gallier. Linear-time Algorithms for Testing the Satisfiablity of Propositional Horn Formulae. J. Logic Programming, 3:267–284, 1984.

    Article  Google Scholar 

  19. O. Dubois. On the r,s-SAT satisfiability problem and a conjecture of Tovey. Discrete Applied Mathematics, 26:51–60, 1990.

    Article  Google Scholar 

  20. O. Dubois, P. André, Y. Boufkhad, and J. Carlier. SAT versus UNSAT, 1994. Position paper, DIMACS chalenge on Satisfiability Testing, to appear.

    Google Scholar 

  21. O. Dubois and J. Carlier. Sur le problème de satisfiabilité. Communication at the Barbizon Workshop on SAT, October 1991.

    Google Scholar 

  22. S. Even, A. Itai, and A. Shamir. On the Complexity of Timetable and Multicommodity Flow Problems. SIAM J. Comput., 5:691–703, 1976.

    Article  Google Scholar 

  23. G. Gallo and M.G. Scutella. Polynomially Solvable Satisfiability Problems. Information Processing Letters, 29:221–227, 1988.

    Article  Google Scholar 

  24. G. Gallo and G. Urbani. Algorithms for Testing the Satisfiablity of Propositional Formulae. Journal of Logic Programming, 7:45–61, 1989.

    Article  Google Scholar 

  25. M.R. Garey and D.S. Johnson. Computer and Intractability: A Guide to the Theory of NP-Completeness. Freeman, San Fransisco, 1979.

    Google Scholar 

  26. I.P. Gent and T. Walsh. The SAT Phase Transition. In A.G. Cohn, editor, Proceedings of 11th European Conference on Artificial Intelligence, ECAI'94, pages 105–109. Wiley, 1994.

    Google Scholar 

  27. M. Ghallab and E. Escalada-Imaz. A linear control algorithm for a class of rule-based systems. Journal of Logic Programming, 11:117–132, 1991.

    Article  Google Scholar 

  28. A. Goerdt. A treshold for unsatifiability. In I.M. Havel and V. Koubek, editors, Proceedings of Mathematical Foundations of Computer Science, MFCS'92, pages 264–272, August 1994.

    Google Scholar 

  29. P. Hansen and B. Jaumard. Uniquely solvable quadratic boolean equations. Discrete Applied Mathematics, 12:147–154, 1985.

    Article  Google Scholar 

  30. J.-J. Hebrard. A linear algorithm for renaming a set of clauses as a Horn set. Theoretical Computer Science, 124:343–350, 1994.

    Article  Google Scholar 

  31. L. Henschen and L. Wos. Unit refutations and Horn sets. JACM, 21(4):590–605, October 1974.

    Article  Google Scholar 

  32. J.N. Hooker. Solving the Incremental Satisfiability Problem. Journal of Logic Programming, 15:177–186, 1993.

    Article  Google Scholar 

  33. S. Jeannicot, L. Oxusoff, and A. Rauzy. Évaluation Sémantique en Calcul Propositionnel. Revue d'Intelligence Artificielle, 2:41–60, 1988.

    Google Scholar 

  34. R.J. Jeroslow and J. Wang. Solving Propositional Satisfiability Problems. Annals of Mathematics and Artificial Intelligence, 1:167–188, 1990.

    Article  Google Scholar 

  35. D.S. Johnson. A Catalog of Complexity Classes. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, volume A. Elsevier, 1990.

    Google Scholar 

  36. D.E. Knuth. Nested Satisfiability. Acta Informatica, 28, 1990.

    Google Scholar 

  37. T. Larrabee. Test Pattern Generation Using Boolean Satisfiability. IEEE Transactions on Computer-Aided Design, 11(1):4–15, January 1992.

    Article  Google Scholar 

  38. T. Larrabee and Y. Tsuji. Evidence for a satisfiability threshold for random 3cnf formulas. In H. Hirsh and al., editors, Proceedings of Spring Symposium on Artificial Intelligence and NP-Hard Problems (Stanford CA 1993), pages 112–118, 1993.

    Google Scholar 

  39. H.R. Lewis. Renaming a Set of Clauses as a Horn Set. JACM, 25(1):134–135, 1978.

    Article  Google Scholar 

  40. G. Lindhorst and F. Shahroki. On renaming a set of clauses as a Horn set. Information Processing Letters, 30:289–293, 1989.

    Article  Google Scholar 

  41. D. Loveland. Automated Theorem Proving: A Logical Basis. North Holland, 1978.

    Google Scholar 

  42. E.L. Lozinskii. A simple test improves checking satisfiability. Journal of Logic Programming, 15:99–111, 1993.

    Article  Google Scholar 

  43. H. Mannila and K. Mehlorn. A fast algorithm for renaming a set of clauses as a Horn set. Information Processing Letters, 21:269–272, 1985.

    Article  Google Scholar 

  44. M. Minoux. LTUR: A Simplified Linear-Time Unit Resolution Algorithm for Horn Formulae and its Computer Implementation. Information Processing Letter, 29:1–12, 1988.

    Article  Google Scholar 

  45. D. Mitchell, B. Selman, and H. Levesque. Hard and Easy Distributions of SAT Problems. In Proceedings Tenth National Conference on Artificial Intelligence (AAAI'92), 1992.

    Google Scholar 

  46. B. Monien and E. Speckenmeyer. Solving Satisfiability in Less than 2n Steps. Discrete Applied Math., 10:287–295, 1985.

    Article  Google Scholar 

  47. R. Petreschi and B. Simeone. Experimental Comparison on 2-Satisfiability Algorithms. RAIRO Recherche Opérationelle, 25:241–264, 8 1991.

    Google Scholar 

  48. D. Pretolani. A linear time algorithm for unique Horn satisfiability. Information Processing Letters, 48:61–66, 1993.

    Article  Google Scholar 

  49. A. Rauzy. On the Complexity of the Davis and Putnam's Procedure on Some Polynomial Sub-Classes of SAT. Technical Report 806-94, LaBRI, URA CNRS 1304, Université Bordeauxl, 9 1994.

    Google Scholar 

  50. M.G. Scutella. A Note on Dowling and Gallier's Top-Down Algorithm for Propositional Horn Satisfiability. Journal of Logic Programming, 8:265–273, 1990.

    MathSciNet  Google Scholar 

  51. B. Selman, H. Levesque, and D. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Proceedings of the 10th National Conference on Artificial Intelligence (AAAI'92), 1992.

    Google Scholar 

  52. R.E. Tarjan. Depth First Search and Linear Graph Algorithms. SIAM J. Comput., 1:146–160, 1972.

    Article  Google Scholar 

  53. C. A. Tovey. A Simplified NP-complete Satisfiability Problem. Discrete Applied Mathematics, 8:85–89, 1984.

    Article  Google Scholar 

  54. A. van Gelder. Linear Time Unit Resolution for Propositional Formulas — in Prolog, Yet. submitted to the Journal of Logic Programming, 1994.

    Google Scholar 

  55. S. Yamasaki and S. Doshita. The satisfiability problem for a class consisting of horn sentences and some non-horn sentences in propositional logic. Information and Computation, 59:1–12, 1983.

    Google Scholar 

  56. R. Zabih and D. Mac Allester. A rearrangement search strategy for determining propositional satisfiability. In Proceedings of the National Conference on Artificial Intelligence, AAAI'88, pages 155–160, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LaBRI-CNRS URA 1304, Université Bordeaux I, 51, cours de la Libération, F-33405, Talence, France

    Antoine Rauzy

Authors
  1. Antoine Rauzy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ugo Montanari Francesca Rossi

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rauzy, A. (1995). Polynomial restrictions of SAT: What can be done with an efficient implementation of the Davis and Putnam's procedure?. In: Montanari, U., Rossi, F. (eds) Principles and Practice of Constraint Programming — CP '95. CP 1995. Lecture Notes in Computer Science, vol 976. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60299-2_31

Download citation

  • DOI: https://doi.org/10.1007/3-540-60299-2_31

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60299-6

  • Online ISBN: 978-3-540-44788-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation