Advertisement

Journal of Heuristics

, Volume 13, Issue 6, pp 587–639 | Cite as

Modelling the dynamics of stochastic local search on k-sat

  • Nicolas G. Fournier
Article

Abstract

A new analytical tool is presented to provide a better understanding of the search space of k-sat. This tool, termed the local value distribution , describes the probability of finding assignments of any value q′ in the neighbourhood of assignments of value q. The local value distribution is then used to define a Markov model to model the dynamics of a corresponding stochastic local search algorithm for k-sat. The model is evaluated by comparing the predicted algorithm dynamics to experimental results. In most cases the fit of the model to the experimental results is very good, but limitations are also recognised.

Keywords

Algorithm analysis Experimental evaluation Stochastic algorithms Local search k-sat 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aarts, E.H.L., Lenstra, J.K.: Local Search in Combinatorial Optimisation. Wiley-Interscience Series in Discrete Mathematics and Optimization. Wiley, Chichester (1997) Google Scholar
  2. Asselmeyer, T., Ebeling, W., Rosé, H.: Smoothing representation of fitness landscapes—the genotype–phenotype map of evolution. BioSystems 39(1), 63–76 (1996) CrossRefGoogle Scholar
  3. Aytemiz, T.: A probabilistic study of 3-satisfiability. Ph.D. thesis, Virginia Polytechnic Institute and State University (2001) Google Scholar
  4. Bäck, T., Eiben, Á.E., Vink, M.E.: A superior evolutionary algorithm for 3-sat. In: Porto, V.W., Saravanan, N., Waagen, D.E., Eiben, Á.E. (eds.) Proceedings of the Seventh Conference on Evolutionary Programming (EP98), San Diego, CA, USA, 1998. Lecture Notes in Computer Science, vol. 1447, pp. 125–136. Springer, Berlin (1998) Google Scholar
  5. Bäck, T., de Graaf, J., Kok, J.N., Kosters, W.A.: Theory of genetic algorithm. In: Phaun, G., Rozenberg, G., Salomaa, A. (eds.) Current Trends in Theoretical Computer Science: Entering the 21st Century, pp. 546–578. World Scientific, Singapore (2001) Google Scholar
  6. Bélaidouni, M., Hao, J.-K.: SAT, local search dynamics and density of states. In: Collet, P., Fonlupt, C., Hao, J.-K., Lutton, E., Schoenauer, M. (eds.) Artificial Evolution, Proceedings of the Fifth International Conference, Evolution Artificielle (EA 2001), Le Creusot, France, 2001. Lecture Notes in Computer Science, vol. 2310, pp. 192–204. Springer, Berlin (2001) Google Scholar
  7. Beyer, H.-G.: Toward a theory of evolution strategies: some asymptotical results from the ( \(1\stackrel{+}{,}\lambda\) )-theory. Evol. Comput. 1(2), 165–188 (1993) Google Scholar
  8. Beyer, H.-G.: Toward a theory of evolution strategies: the (μ,λ)-theory. Evol. Comput. 2(4), 381–407 (1994a) MathSciNetGoogle Scholar
  9. Beyer, H.-G.: Towards a theory of ‘evolution strategies’: results for \((1\stackrel{+}{,}\lambda)\) -strategies on (nearly) arbitrary fitness functions. In: Davidor, Y., Schwefel, H.-P., Männer, R. (eds.) Proceedings of the Third International Conference on Parallel Problem Solving from Nature (PPSN III), Jerusalem, Israel. Lecture Notes in Computer Science, vol. 866, pp. 58–67. Springer, Berlin (1994b) Google Scholar
  10. Beyer, H.-G.: Toward a theory of evolution strategies: on the benefits of sex—the (μ/μ, λ)-theory. Evol. Comput. 3(1), 81–111 (1995) MathSciNetGoogle Scholar
  11. Brueggemann, T., Kern, W.: An improved deterministic local search algorithm for 3-SAT. Theor. Comput. Sci. 329(1–3), 303–313 (2004) MATHCrossRefMathSciNetGoogle Scholar
  12. Cheeseman, P., Kanefsky, B., Taylor, W.M.: Where the really hard problems are. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI-91), Sydney, Australia, pp. 331–337. Morgan Kaufmann, Los Altos (1991) Google Scholar
  13. Clark, D.A., J. Frank, I.P., Gent, E., MacIntyre, T., Tomov, N., Walsh, T.: Local search and the number of solutions. In: Freuder, E.C. (ed.) Proceedings of Second International Conference on Principles and Practices of Constraint Programming (CP-96), Cambridge, MA, USA. Lecture Notes in Computer Science, vol. 1118, pp. 119–133. Springer, Berlin (1996) Google Scholar
  14. Croes, G.A.: A method for solving travelling-salesman problems. Oper. Res. 6, 791–812 (1958) MathSciNetGoogle Scholar
  15. Dantsin, E., Goerdt, A., Hirsch, E.A., Kannan, R., Kleinberg, J., Papadimitriou, C., Raghavan, P., Schöning, U.: A deterministic (2−2/(k+1))n algorithm for k-sat based on local search. In: Rolim, J.D.P., Powell, O., Schütz, F., Sosnowska, D., Zwissig, T. (eds.) Proceedings of the Twenty-Seventh International Colloquium on Automata, Languages and Programming (ICALP 2000), pp. 236–247. Geneva, Switzerland, 2000. Theoretical Computer Science, to appear Google Scholar
  16. Eiben, Á.E., Rudolph, R.: Theory of evolutionary algorithms: a birds eye view. Theor. Comput. Sci. 229, 3–9 (1999) MATHCrossRefMathSciNetGoogle Scholar
  17. Eiben, Á.E., van der Hauw, J.K.: Solving 3-SAT by GAs adapting constraint weights. In: Proceedings of the IEEE International Conference on Evolutionary Computation (ICEC), pp. 81–86. IEEE, New York (1997) CrossRefGoogle Scholar
  18. Feller, W.: An Introduction to Probability Theory and its Applications, vol. I, revised 3rd edn. Wiley, New York (1970) Google Scholar
  19. Flood, M.M.: The travelling salesman problem. Oper. Res. 4, 61–75 (1956) MathSciNetCrossRefGoogle Scholar
  20. Frank, J.D.: Weighting for Godot: Learning heuristics for GSAT. In: Weld, D., Clancey, B. (eds.) Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI-96), Portland, OR, USA, pp. 338–343. AAAI (1996) Google Scholar
  21. Garey, M.R., Johnson, D.S.: Computers and Intractability: a Guide to the Theory of NP-Completeness Freeman, New York (1979) MATHGoogle Scholar
  22. Gent, I.P., Walsh, T.: The enigma of SAT hill-climbing procedures. Technical report 605, University of Edinburgh, Department of Artificial Intelligence (1992) Google Scholar
  23. Gent, I.P., Walsh, T.: An empirical analysis of search in GSAT. J. Artif. Intell. Res. 1, 47–59 (1993a) MATHGoogle Scholar
  24. Gent, I.P., Walsh, T.: Towards an understanding of hill-climbing procedures for SAT. In: Fikes, R., Lehnert, W. (eds.) Proceedings of the Eleventh National Conference on Artificial Intelligence (AAAI-93), Washington, DC, USA, pp. 28–33. AAAI Press/The MIT Press, Menlo Park (1993b) Google Scholar
  25. Gent, I.P., Walsh, T.: The search for satisfaction. Technical report. University of Edinburgh. http://dream.dai.ed.ac.uk/group/tw/sat/sat-survey2.ps (visited 18 September 2001) (1999)
  26. Gent, I.P., MacIntyre, E., Prosser, P., Walsh, T.: The constrainedness of search. In: Weld, D., Clan- cey, B. (eds.) Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI-96), Portland, OR, USA, pp. 246–252. AAAI Press/The MIT Press, Menlo Park (1996) Google Scholar
  27. Gent, I.P., MacIntyre, E., Prosser, P., Walsh, T.: The scaling of search cost. In: Kuipers, B.J., Webber, B. (eds.) Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI-97), Providence, RI, USA, pp. 315–320. AAAI Press/The MIT Press, Menlo Park (1997) Google Scholar
  28. Glover, F.W.: Future paths for integer programming and links to artificial intelligence. Comput. Oper. Res. 13, 533–549 (1986) MATHCrossRefMathSciNetGoogle Scholar
  29. Glover, F.W., Laguna, M.: Tabu search. In: Reeves, C.R. (ed.) Modern Heuristic Techniques for Combinatorial Problems, pp. 70–150. Blackwell Scientific, Oxford (1993) Google Scholar
  30. Gottlieb, J., Marchiori, E., Rossi, C.: Evolutionary algorithms for the satisfiability problem. Evol. Comput. 10(1), 35–50 (2002) CrossRefGoogle Scholar
  31. Gottlieb, J., Voss, N.: Improving the performance of evolutionary algorithms for the satisfiability problem by refining functions. In: Eiben, Á.E., Bäck, T., Schoenauer, M., Schwefel, H.-P. (eds.) Proceedings of the Fifth International Conference on Parallel Problem Solving from Nature (PPSN V), Amsterdam, The Netherlands. Lecture Notes in Computer Science, vol. 1498, pp. 755–764. Springer, Berlin (1998) CrossRefGoogle Scholar
  32. Gu, J.: Efficient local search for very large-scale satisfiability problems. SIGART Bull. 3(1), 8–12 (1992) CrossRefGoogle Scholar
  33. Håstad, J.: Some optimal inapproximability results. J. ACM 48(4), 798–859 (2001) CrossRefMathSciNetMATHGoogle Scholar
  34. Hansen, P., The steepest ascent mildest descent heuristic for combinatorial programming. Presented at the Congress on Numerical Methods in Combinatorial Optimisation, Capri, Italy, 1986 Google Scholar
  35. Hansen, P., Jaumard, B.: Algorithms for the maximum satisfiability problem. Computing 44, 279–303 (1990) MATHCrossRefMathSciNetGoogle Scholar
  36. Hastings, W.K.: Monte Carlo sampling methods using Markov chains and their applications. Biometrika 57(1), 97–109 (1970) MATHCrossRefGoogle Scholar
  37. Hofmeister, T., Schöning, U., Schuler, R., Watanabe, O.: A probabilistic 3-sat algorithm further improved. In: H. Alt, A. Ferreira (eds.) Proceedings of the 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS 02), Antibes, Juan les Pins, France. Lecture Notes in Computer Science, vol. 2285, pp. 192–202. Springer, Berlin (2002). Google Scholar
  38. Hoos, H.H.: Stochastic local search-methods, models, applications. Ph.D. thesis, Technische Universität Darmstadt (1998) Google Scholar
  39. Hoos, H.H.: An adaptive noise mechanism for WalkSAT. In: Dechter, R., Kearns, M., Sutton, R. (eds.) Proceedings of the Eighteenth national conference on Artificial Intelligence (AAAI-02), Edmonton, AB, Canada, pp. 655–660. AAAI Press/The MIT Press, Menlo Park (2002a) Google Scholar
  40. Hoos, H.H.: A mixture-model for the behaviour of SLS algorithms for SAT. In: Dechter, R., Kearns, M., Sutton, R. (eds.) Proceedings of the Eighteenth national conference on Artificial Intelligence (AAAI-02), Edmonton, AB, Canada, pp. 661–667. AAAI Press/The MIT Press, Menlo Park (2002b) Google Scholar
  41. Hoos, H.H., Stützle, T.: Local search algorithms for SAT: An empirical evaluation. J. Autom. Reason. 24(4), 421–481 (2000) MATHCrossRefGoogle Scholar
  42. Hoos, H.H., Stützle, T.: SATLIB—the satisfiability library. http://www.satlib.org/ (2003)
  43. Hutter, F., Tompkins, D.A.D., Hoos, H.H.: Scaling and probabilistic smoothing: Efficient dynamic local search for SAT. In: Hentenryck, P.V. (ed.) Principles and Practice of Constraint Programming (CP 2002), Ithaca, NY, USA. Lecture Notes in Computer Science, vol. 2470, pp. 233–248. Springer, Berlin (2002) CrossRefGoogle Scholar
  44. Iwama, K., Tamaki, S.: Improved upper bounds for 3-sat. In: Proceedings of the 15th Annual ACM–SIAM Symposium on Discrete Algorithms (SODA 04), New Orleans, LA, USA, p. 328. ACM, New York (2004) Google Scholar
  45. Johnson, D.S.: Challenges for theoretical computer science: Draft. http://www.research.att.com/~dsj/nsflist.html (visited 2 April 2003) (2000)
  46. Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov Chains. Graduate Texts in Mathematics, vol. 40, 2nd edn. Springer, New York (1976) MATHGoogle Scholar
  47. Kirkpatrick, S., Selman, B.: Critical behaviour in the satisfiability of random Boolean formulae. Science 264(5163), 1297–1301 (1994) CrossRefMathSciNetGoogle Scholar
  48. Kirkpatrick, S., Toulouse, G.: Configuration space analysis of travelling salesman problems. J. Phys. 46(8), 1277–1292 (1985) MathSciNetGoogle Scholar
  49. Lundy, M., Mees, A.I.: Convergence of an annealing algorithm. Math. Program. 34, 111–124 (1986) MATHCrossRefMathSciNetGoogle Scholar
  50. Marchiori, E., Rossi, C.: A flipping genetic algorithm for hard 3-sat problems. In: Banzhaf, W., Daida, J., Eiben, A.E., Garzon, M.H., Honavar, V., Jakiela, M., Smith, R.E. (eds.) Proceedings of the Genetic and Evolutionary Computation Conference, vol. 1, Orlando, FL, USA, pp. 393–400. Morgan Kaufmann, Los Altos (1999) Google Scholar
  51. Metropolis, N., Rosenbluth, A.W., Rosenbluth, M.N., Teller, A.H., Teller, E.: Equations of state calculations by fast computing machines. J. Chem. Phys. 21(6), 1087–1092 (1953) CrossRefGoogle Scholar
  52. Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995) MATHGoogle Scholar
  53. Norris, J.R.: Markov Chains. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (1997) MATHGoogle Scholar
  54. Papadimitriou, C.H.: On selecting a satisfying truth assignment. In: Proceedings of the 33nd Annual IEEE Symposium on Foundations of Computer Science (FOCS 91), San Juan, Puerto Rico, pp. 163–169. IEEE, New York (1991) Google Scholar
  55. Parkes, A.J.: Clustering at the phase transition. In: Kuipers, B.J., Webber, B. (eds.) Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI-97), Providence, RI, USA, pp. 340–345. AAAI (1997) Google Scholar
  56. Parkes, A.J., Walser, J.P.: Tuning local search for satisfiability testing. In: Weld, D., Clancey, B. (eds.) Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI-96), Portland, Oregon, USA, pp. 365–362. AAAI (1996) Google Scholar
  57. Prügel-Bennett, A., Shapiro, J.L.: Analysis of genetic algorithms using statistical mechanics. Phys. Rev. Lett. 72(9), 1305–1309 (1994) CrossRefGoogle Scholar
  58. Rana, S., Whitley, L.D: Genetic algorithm behavior in the MAXSAT domain. In: Eiben, Á.E., Bäck, T., Schoenauer, M., Schwefel, H.-P. (eds.) Proceedings of the Fifth International Conference on Parallel Problem Solving from Nature (PPSN V), Amsterdam, The Netherlands. Lecture Notes in Computer Science, vol. 1498, pp. 755–764. Springer, Berlin (1998) CrossRefGoogle Scholar
  59. Rechenberg, I.: Optimierung Technischer Systeme nach den Prinzipien der biologischen Evolution. Frommann-Holzboog, Stuttgart. Ph.D. thesis, Technische Universität Berlin (1970) Google Scholar
  60. Reeves, C.R., Rows, J.E.: Genetic Algorithms—Principles and Perspectives. Operations Research/Computer Science Interfaces, vol. 20. Kluwer, Norwell (2003) Google Scholar
  61. Rossi, C., Marchiori, E., Kok, J.N.: An adaptive evolutionary algorithm for the satisfiability problem. In: Carroll, J., Damiani, E., Haddad, H., Oppenheim, D. (eds.) Proceedings of the 2000 ACM Symposium on Applied Computing, vol. 1, Como, Italy, pp. 463–469. ACM, New York (2000) CrossRefGoogle Scholar
  62. Sasaki, G.H., Hajek, B.: The time complexity of maximum matching by simulated annealing. J. ACM 35(2), 387–403 (1988) CrossRefMathSciNetGoogle Scholar
  63. Schöning, U.: A probabilistic algorithm for k-SAT and constraint satisfaction problems. In: Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science (FOCS 99), New York, USA, pp. 410–414. IEEE, New York (1999) Google Scholar
  64. Schwefel, H.-P.: Evolutionsstrategie und numerische Optimierung. Ph.D. thesis, Technische Universität Berlin (1974) Google Scholar
  65. Schwefel, H.-P.: Evolution and Optimum Seeking. Wiley, New York (1995) Google Scholar
  66. Selman, B., Kautz, H.A.: Domain-independent extensions to GSAT: Solving large structured satisfiability problems. In: Bajcsy, R. (ed.) Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI-93), Chambéry, France, pp. 290–295. Morgan Kaufmann, Los Altos, (1993) Google Scholar
  67. Selman, B., Levesque, H.J., Mitchell, D.G.: A new method for solving hard satisfiability problems. In: Rosenbloom, P., Szolovits, P. (eds.) Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), San Jose, California, USA, pp. 440–446. AAAI Press/The MIT Press, Menlo Park (1992) Google Scholar
  68. Stadler, P.F.: Towards a theory of landscapes. In: Lopéz-Peña, R., Capovilla, R., García-Pelayo, R., Waelbroeck, H., Zertuche, F. (eds.) Complex Systems and Binary Networks. Lecture Notes in Physics, vol. 461, pp. 77–163. Springer, Berlin (1995) Google Scholar
  69. Thornton, J., Nghia Pham, D., Bain, S., Ferreira Jr., V.: Additive versus multiplicative clause weighting for SAT. In: Deborah, G.F., McGuinness, L. (eds.) Proceedings of the Nineteenth National Conference on Artificial Intelligence (AAAI-04), San Jose, CA, USA, pp. 191–196. AAAI Press/The MIT Press, Menlo Park (2004) Google Scholar
  70. Vose, M.D.: Simple Genetic Algorithms. Morgan Kaufmann, California (1999) Google Scholar
  71. Watson, J.-P., Whitley, L.D., Howe, A.E.: A dynamic model of the tabu search for the job-shop scheduling problem. In: Kendall, G. (ed.) Conference Proceedings of the Multidisciplinary International Conference on Scheduling (MISTA03), Nottingham, UK, 2003, pp. 320–336 Google Scholar
  72. Wu, Z., Wah, B.W.: An efficient global-search strategy in discrete Lagrangian methods for solving hard satisfiability problems. In: Kautz, H.A., Porter, B. (eds.) Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI-00), Austin, TX, USA, pp. 310–315. AAAI Press/The MIT Press, Menlo Park (2000) Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2007

Authors and Affiliations

  1. 1.EPOMunichGermany

Personalised recommendations