Skip to main content
Log in

Penalty Formulations and Trap-Avoidance Strategies for Solving Hard Satisfiability Problems

  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

In this paper we study the solution of SAT problems formulated as discrete decision and discrete constrained optimization problems. Constrained formulations are better than traditional unconstrained formulations because violated constraints may provide additional forces to lead a search towards a satisfiable assignment. We summarize the theory of extended saddle points in penalty formulations for solving discrete constrained optimization problems and the associated discrete penalty method (DPM). We then examine various formulations of the objective function, choices of neighborhood in DPM, strategies for updating penalties, and heuristics for avoiding traps. Experimental evaluations on hard benchmark instances pinpoint that traps contribute significantly to the inefficiency of DPM and force a trajectory to repeatedly visit the same set of or nearby points in the original variable space. To address this issue, we propose and study two trap-avoidance strategies. The first strategy adds extra penalties on unsatisfied clauses inside a trap, leading to very large penalties for unsatisfied clauses that are trapped more often and making these clauses more likely to be satisfied in the future. The second strategy stores information on points visited before, whether inside traps or not, and avoids visiting points that are close to points visited before. It can be implemented by modifying the penalty function in such a way that, if a trajectory gets close to points visited before, an extra penalty will take effect and force the trajectory to a new region. It specializes to the first strategy because traps are special cases of points visited before. Finally, we show experimental results on evaluating benchmarks in the DIMACS and SATLIB archives and compare our results with existing results on GSAT, WalkSAT, LSDL, and Grasp. The results demonstrate that DPM with trap avoidance is robust as well as effective for solving hard SAT problems.

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

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Shang Y, Wah B W. A discrete Lagrangian based global search method for solving satisfiability problems. J. Global Optimization, January 1998, 12(1): 61–99.

    Google Scholar 

  2. Barth P. A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization. Technical Report MPI-I-95-2-003, Max-Planck-Institute fur Informatik, 1995.

  3. Robinson J A. A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach., 1965, pp. 23–41.

  4. Genesereth M R, Nilsson N J. Logical Foundation of Artificial Intelligence. Morgan Kaufmann, 1987.

  5. Davis M, Putnam H. A computing procedure for quantification theory. J. Assoc. Comput. Mach., 1960, 7: 201–215.

    Google Scholar 

  6. Purdom P W. Search rearrangement backtracking and polynomial average time. Artificial Intelligence, 1983, 21: 117–133.

    Google Scholar 

  7. Gu J, Wang W. A novel discrete relaxation architecture. IEEE Trans. PAMI, August 1992, 14(8): 857–865.

    Google Scholar 

  8. Gu J. The UniSAT problem models (appendix). IEEE Trans. PAMI, Aug 1992, 14(8): 865.

    Google Scholar 

  9. Gu J. Efficient local search for very large-scale satisfiability problems. SIGART Bulletin, January 1992, 3(1): 8–12.

    Google Scholar 

  10. Gu J. Local search for satisfiability (SAT) problems. IEEE Trans. Systems, Man, and Cybernetics, 1993, 23(4): 1108–1129.

    Google Scholar 

  11. Gu J. Global optimization for satisfiability (SAT) problems. IEEE Trans. Knowledge and Data Engineering, Jun 1994, 6(3): 361–381.

    Google Scholar 

  12. Selman B et al. A new method for solving hard satisfiability problems. In Proc. AAAI-92, San Jose, 1992, pp. 440–446.

  13. Selman B, Kautz H, Cohen B. Noise strategies for improving local search. In Proc. 12th National Conf. Artificial Intelligence, Seattle, WA, 1994, pp. 337–343.

  14. Selman B, Kautz H. Domain-independent extensions to GSAT: Solving large structured satisfiability problems. In Proc. 13th Int. Joint Conf. Artificial Intelligence, 1993, pp. 290–295.

  15. Selman B et al. Local search strategies for satisfiability testing. In Proc. 2nd DIMACS Challenge Workshop on Cliques, Coloring, and Satisfiability, Rutgers University, 1993, pp. 290–295.

  16. Hoos H H. On the run-time behaviour of stochastic local search algorithms for SAT. In Proc. Sixteenth National Conf. Artificial Intelligence, 1999, pp. 661–666.

  17. Gent I P, Walsh T. An empirical analysis of search in GSAT. Journal of Artificial Intelligence Research, 1993, 1: 25–37.

    Google Scholar 

  18. Glover F. Tabu search — Part I. ORSA J. Computing, 1989, 1(3): 190–206.

    Google Scholar 

  19. Battiti R, Tecchiolli G. The reactive tabu search. ORSA Journal on Computing, 1994, 6(2): 126–140.

    Google Scholar 

  20. Morris P. The breakout method for escaping from local minima. In Proc. 11th National Conf. Artificial Intelligence, Washington DC, 1993, pp. 40–45.

  21. Frank J. Learning short-term weights for GSAT. In Proc. 15th Int. Joint Conf. AI, 1997, pp. 384–391.

  22. Fukunaga A. Efficient implementations of SAT local search. In Proc. 7th Int. Conf. Theory and Applications of Satisfiability Testing, 2004.

  23. Van Hentenryck P, Michel L. Control abstractions for local search. In Proc. the Ninth Int. Conf. Principles and Practice of Constraint Programming, LNCS 2833, 2003, pp. 65–80.

  24. Zhang L, Malik S. Towards symmetric treatment of conflicts and satisfaction in quantified Boolean satisfiability solver. In Proc. 8th Int. Conf. Principles and Practice of Constraint Programming. Springer Verlag, 2002.

  25. Moskewicz M et al. Chaff: Engineering an efficient SAT solver. In Proc. 39th Design Automation Conf., 2001.

  26. Wah B W, Wang T. Simulated annealing with asymptotic convergence for nonlinear constrained global optimization. In Proc. Principles and Practice of Constraint Programming, Springer-Verlag, October 1999, pp. 461–475.

  27. Folino G et al. Combining cellular genetic algorithms and local search for solving satisfiability problems. In Proc. 10th IEEE Int. Conf. Tools with AI, 1998, pp. 192–198.

  28. Blair C E, Jeroslow R G, Lowe J K. Some results and experiments in programming techniques for propositional logic. Computers and Operations Research, 1986, 13(5): 633–645.

    Google Scholar 

  29. Hooker J N. Resolution vs. cutting plane solution of inference problems: Some computational results. Operations Research Letters, 1988, 7: 1–7.

    Google Scholar 

  30. Kamath A P, Karmarkar N K, Ramakrishnan K G, Resende M G C. Computational experience with an interior point algorithm on the satisfiability problem. Annals of Operations Research, 1990, 25: 43–58.

    Google Scholar 

  31. Shi R C J, Vannelli A, Vlach J. An improvement on Karmarkar’s algorithm for integer programming. COAL Bulletin of the Mathematical Programming Society, 1992, 21: 23–28.

    Google Scholar 

  32. Wah B W, Shang Y. A discrete Lagrangian-based global-search method for solving satisfiability problems. In Satisfiability Problem: Theory and Applications, Ding-Zhu Du, Jun Gu, Panos Pardalos (eds.), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, 1997, pp. 365–392.

    Google Scholar 

  33. Wah B W, Chang Y-J. Trace-based methods for solving nonlinear global optimization problems. J. Global Optimization, March 1997, 10(2): 107–141.

    Google Scholar 

  34. Shang Y, Wah B W. Global optimization for neural network training. IEEE Computer, March 1996, 29(3): 45–54.

    Google Scholar 

  35. Luenberger D G. Linear and Nonlinear Programming. Addison-Wesley, Reading, MA, 1984.

    Google Scholar 

  36. Spellucci P. An SQP method for general nonlinear programs using only equality constrained subproblems. Mathematical Programming, 1998, 82: 413–448.

    Google Scholar 

  37. Wah B W, Wang T. Constrained simulated annealing with applications in nonlinear constrained global optimization. In Proc. Int. Conf. Tools with AI, IEEE, Nov. 1999, pp. 381–388.

  38. Chang Y J et al. Lagrangian techniques for solving a class of zero-one integer linear programs. In Proc. Computer Software and Applications Conf., Dallas, Aug. 1995, IEEE, pp. 156–161.

  39. Wah B, Chen Y X. Fast temporal planning using the theory of extended saddle points for mixed nonlinear optimization. Artificial Intelligence, (accepted for publication) 2005.

  40. Wu Z. Discrete Lagrangian methods for solving nonlinear discrete constrained optimization problems [Thesis]. Dept. Computer Science, Univ. Illinois, Urbana, IL, May 1998.

    Google Scholar 

  41. Wah B W, Wu Z. The theory of discrete Lagrange multipliers for nonlinear discrete optimization. In Proc. Principles and Practice of Constraint Programming, Springer-Verlag, October 1999, pp. 28–42.

  42. Aarts E, Korst J. Simulated Annealing and Boltzmann Machines. J. Wiley and Sons, 1989.

  43. Wu Z. The theory and applications of nonlinear constrained optimization using Lagrange multipliers [Dissertation]. Dept. Computer Science, Univ. Illinois, Urbana, IL, May 2001.

    Google Scholar 

  44. Gent I P et al. Morphing: Combining structure and randomness. In Proc. 16th National Conf. AI, 1999, pp. 654–660

  45. Marques-Silva J P, Sakalla K A. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, May 1999, 48(5): 506–521.

    Google Scholar 

  46. Wu Z, Wah B W. Trap escaping strategies in discrete Lagrangian methods for solving hard satisfiability and maximum satisfiability problems. In Proc. 1999 National Conf. Artificial Intelligence, AAAI, July 1999, pp. 673–678.

  47. Selman B. Private communcation, 1995.

  48. Kautz H, Selman B. Pushing the envelope: Planning, propositional logic, and stochastic search. In Proc. the AAAI National Conf. AI, 1996, pp. 1194–1201.

  49. SATLIB suite. http://www.informatik.tu-darmstadt.de/AI/SATLIB.

  50. Choi K F M et al. A Lagrangian reconstruction of a class of local search methods. In Proc. 10th Int. Conf. Artificial Intelligence Tools, IEEE Computer Society, 1998.

  51. Freeman J W. Improvements to propositional satisfiability search algorithms [Dissertation]. Dept. Computer and Information Science, Univ. Pennsylvania, May 1995.

  52. Dubois O et al. SAT versus UNSAT. In DIMACS Workshop on Satisfiability Testing, New Brunswick, NJ, 1993.

  53. Pretolani D. Efficiency and stability of hypergraph SAT algorithms. In Second DIMACS Implementation Challenge, Johnson D S, Trick M A (eds.), Volume 26, American Mathematical Society, 1993, pp. 479–498.

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Benjamin W. Wah.

Additional information

Supported by the National Science Foundation of USA under Grant No.NSF IIS 03-12084.

Benjamin W. Wah is currently the Franklin W. Woeltge Endowed Professor of Electrical and Computer Engineering and a professor of the Coordinated Science Lab. the Univ. Illinois at Urbana-Champaign, Urbana, IL. He received his Ph.D. degree in computer science from the Univ. California, Berkeley, CA, in 1979. Previously, he had served on the faculty of Purdue Univ. (1979–85), as a Program Director at the National Science Foundation (1988–89), as Fujitsu Visiting Chair Professor of Intelligence Engineering, Univ. Tokyo (1992), and McKay Visiting Professor of Electrical Engineering and Computer Science, Univ. California, Berkeley (1994). In 1989, he was awarded a University Scholar of the University of Illinois; in 1998, he received the IEEE Computer Society Technical Achievement Award; in 2000, the IEEE Millennium Medal; and in 2003, the Raymond T. Yeh Lifetime Achievement Award from the Society for Design and Process Science.

Wah’s current research interests are in the areas of nonlinear search and optimization, multimedia signal processing, and computer networks.

Wah was the Editor-in-Chief of the IEEE Trans. Knowledge and Data Engineering between 1993 and 1996, and is the Honorary Editor-in-Chief of Knowledge and Information Systems. He currently serves on the editorial boards of Information Sciences, Int. J. Artificial Intelligence Tools, J. VLSI Signal Processing, World Wide Web, and Neural Processing Letters. He had chaired a number of international conferences and was the International Program Committee Chair of the IFIP World Congress in 2000. He has served the IEEE Computer Society in various capacities; among them include Vice President for Publications (1998 and 1999) and President (2001). He is a Fellow of the IEEE, AAAS, ACM, and the Society for Design and Process Science.

Zhe Wu was born on Jan. 4, 1974. He received his B.Sc. degree (June 1996) in the Dept. Special Class for Gifted Young from the Univ. Science and Technology of China and M.S. degree (May 1998) and Ph.D. degree (June 2001) from the Dept. Computer Science of the Univ. Illinois at Urbana-Champaign. He is currently working as a principal member of technical staff in the Oracle UDDI Server Team in Oracle Co. His main research interests are in optimization, signal processing, software engineering and computer networks.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Wah, B.W., Wu, Z. Penalty Formulations and Trap-Avoidance Strategies for Solving Hard Satisfiability Problems. J Comput Sci Technol 20, 3–17 (2005). https://doi.org/10.1007/s11390-005-0002-8

Download citation

  • Received:

  • Revised:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11390-005-0002-8

Keywords

Navigation