Advertisement

Look-ahead versus look-back for satisfiability problems

  • Chu Min Li
  • Anbulagan
Session 5b
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1330)

Abstract

CNF propositional satisfiability (SAT) is a special kind of the more general Constraint Satisfaction Problem (CSP). While lookback techniques appear to be of little use to solve hard random SAT problems, it is supposed that they are necessary to solve hard structured SAT problems. In this paper, we propose a very simple DPL procedure called Satz which only employs some look-ahead techniques: a variable ordering heuristic, a forward consistency checking (Unit Propagation) and a limited resolution before the search, where the heuristic is itself based on unit propagation. Satz is favorably compared on random 3-SAT problems with three DPL procedures among the best in the literature for these problems. Furthermore on a great number of problems in 4 well known SAT benchmarks Satz reaches or outspeeds the performance of three other DPL procedures among the best in the literature for structured SAT problems. The comparative results suggest that a suitable exploitation of look-ahead techniques, while very simple and efficient for random SAT problems, may allow to do without sophisticated look-back techniques in a DPL procedure.

Keywords

Search Tree Unit Propagation Conjunctive Normal Form Unit Clause Conjunctive Normal Form Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bayardo Jr. R.J., Schrag R.C., Using CSP Look-Back Techniques to Solve Exceptionally Hard SAT Instances, Proceedings of the Second International Conference on Principles and Practice of Constraint Programming (CP96), Cambridge, Massachusetts, USA, August 1996.Google Scholar
  2. 2.
    Bayardo Jr. R.J., Schrag R.C., Using CSP Look-Back Techniques to Solve Real-World SAT Instances, to appear in proceedings of AAAI-97, Providence, Rhode Island, July 1997.Google Scholar
  3. 3.
    Billionnet A., Sutter A., An efficient algorithm for 3-satisfiability problem, Operations Research Letters, 12:29–36, July 1992.Google Scholar
  4. 4.
    Cook S.A., The Complexity of Theorem Proving Procedures, Proceedings of 3rd ACM Symp. on Theory of Computing, Ohio, 1971, pp. 151–158.Google Scholar
  5. 5.
    Crawford J.M., Auton L.D., Experimental results on the Crossover point in Random 3-SAT,Artificial Intelligence, No. 81, 1996.Google Scholar
  6. 6.
    Davis M., Logemann G., Loveland D., A machine program for theorem proving, Commun. ACM 5, 1962, pp. 394–397.Google Scholar
  7. 7.
    Dubois O., Andre P., Boufkhad Y., Carlier J., SAT versus UNSAT. Second DIMACS Implementation Challenge, D. S. Johnson and M. A. Trick (eds.), 1993.Google Scholar
  8. 8.
    Freeman J.W., Improvements to propositional satisfiability search algorithms, Ph.D. Thesis, Department of computer and Information science, University of Pennsylvania, Philadelphia, PA, 1995.Google Scholar
  9. 9.
    Gloess P.Y., U-Log, a Unified Object Logic, Revue d'intelligence artificielle, Vol. 5, No. 3, 1991, pp. 33–66.Google Scholar
  10. 10.
    Hooker J.N., Vinay V., Branching rules for satisfiability, Journal of Automated Reasoning, 15:359–383, 1995.Google Scholar
  11. 11.
    Jeroslow R., Wang J., Solving propositional satisfiability problems, Annals of Mathematics and AI 1, 1990, pp. 167–187.Google Scholar
  12. 12.
    Kim S., Zhang H., ModGen: Theorem proving by model generation, Proceedings of the 12th National Conference on Artificial Intelligence (AAAI-94), 1994, pp. 162–167.Google Scholar
  13. 13.
    Li C.M., Exploiting yet more the power of unit clause propagation to solve 3-SAT problem, Proceedings of the ECAI'96 Workshop on Advances in Propositional Deduction, Budapest, Hungary, August 1996, pp. 11–16.Google Scholar
  14. 14.
    Li C.M., Anbulagan, Heuristics Based on Unit Propagation for Satisfiability Problems, to appear in Proceedings of IJCAI'97, Nagoya, Japan, August 1997.Google Scholar
  15. 15.
    Mitchell D., Selman B., Levesque H., Hard and Easy Distributions of SAT Problems, Proceedings of the 10th National Conference on Artificial Intelligence (AAAI-92), San Jose, CA, July 1992, pp. 459–465.Google Scholar
  16. 16.
    Pretolani D., Satisfiability and hypergraphs, Ph.D. Thesis, Dipartimento di Informatica, Università di Pisa, 1993.Google Scholar
  17. 17.
    Silva J. P. M., Sakallah K. A., Conflict Analysis in Search Algorithms for Propositional Satisfiability, Proceedings of the International Conference on Tools with Artificial Intelligence, November 1996.Google Scholar
  18. 18.
    Stephan P. R., Brayton R. K., Sangiovanni-Vincentelli A. L., Combinational Test Generation Using Satisfiability, Memorandum No. UCB/ERL M92/112, EECS Department, University of California at Berkeley, October 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Chu Min Li
    • 1
  • Anbulagan
    • 1
  1. 1.LaRIA, Université de Picardie Jules VerneAmiens Cédex 01France

Personalised recommendations