Document Open Access Logo

Effect of Initial Assignment on Local Search Performance for Max Sat

Authors Daniel Berend, Yochai Twitto

PDF
Thumbnail PDF

File

LIPIcs.SEA.2020.8.pdf
  • Filesize: 0.69 MB
  • 14 pages

Document Identifiers

Author Details

Daniel Berend
  • Departments of Mathematics and of Computer Science, Ben-Gurion University, Beer Sheva 84105, Israel
Yochai Twitto
  • Department of Computer Science, Ben-Gurion University, Beer Sheva 84105, Israel

Funding

This research was partially supported by the Milken Families Foundation Chair in Mathematics and by the Lynne and William Frankel Center for Computer Science.

Acknowledgements

We thank Shaowei Cai for providing us access to the original authors' implementation of the CCLS solver used in Max Sat Evaluation 2016, and André Abramé for providing us access to the Abramé-Habet benchmark used (partially) in that evaluation. We also thank Gregory Gutin and Shahar Golan for their helpful comments on this paper.

Cite AsGet BibTex

Daniel Berend and Yochai Twitto. Effect of Initial Assignment on Local Search Performance for Max Sat. In 18th International Symposium on Experimental Algorithms (SEA 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 160, pp. 8:1-8:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.SEA.2020.8

Abstract

In this paper, we explore the correlation between the quality of initial assignments provided to local search heuristics and that of the corresponding final assignments. We restrict our attention to the Max r-Sat problem and to one of the leading local search heuristics - Configuration Checking Local Search (CCLS). We use a tailored version of the Method of Conditional Expectations (MOCE) to generate initial assignments of diverse quality. We show that the correlation in question is significant and long-lasting. Namely, even when we delve deeper into the local search, we are still in the shadow of the initial assignment. Thus, under practical time constraints, the quality of the initial assignment is crucial to the performance of local search heuristics. To demonstrate our point, we improve CCLS by combining it with MOCE. Instead of starting CCLS from random initial assignments, we start it from excellent initial assignments, provided by MOCE. Indeed, it turns out that this kind of initialization provides a significant improvement of this state-of-the-art solver. This improvement becomes more and more significant as the instance grows.

Subject Classification

ACM Subject Classification
  • Theory of computation → Theory of randomized search heuristics
  • Theory of computation → Stochastic approximation
Keywords
  • Combinatorial Optimization
  • Maximum Satisfiability
  • Local Search
  • Probabilistic Algorithms

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. André Abramé, Djamal Habet, and Donia Toumi. Improving configuration checking for satisfiable random k-sat instances. Annals of Mathematics and Artificial Intelligence, 79(1-3):5-24, 2017. Google Scholar
  2. Dimitris Achlioptas and Yuval Peres. The threshold for random k-sat is 2^k log 2 - o(k). Journal of the American Mathematical Society, 17(4):947-973, 2004. Google Scholar
  3. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. Sat-based maxsat algorithms. Artificial Intelligence, 196:77-105, 2013. Google Scholar
  4. Josep Argelich, Chu Min Li, Felip Manyà, and Jordi Planes. Maxsat evaluations. URL: http://www.maxsat.udl.cat/.
  5. Giorgio Ausiello, Pierluigi Crescenzi, Giorgio Gambosi, Viggo Kann, Alberto Marchetti-Spaccamela, and Marco Protasi. Complexity and Approximation: Combinatorial Optimization Problems and Their Approximability Properties. Springer-Verlag, 2 edition, 2003. Google Scholar
  6. Daniel Berend and Yochai Twitto. The normalized autocorrelation length of random max r-sat converges in probability to (1-1/2^r)/r. In The 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016), pages 60-76. Springer, 2016. Google Scholar
  7. Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of Satisfiability, volume 185. IOS press, 2009. Google Scholar
  8. Noureddine Bouhmala. A variable neighborhood walksat-based algorithm for max-sat problems. The Scientific World Journal, 2014, 2014. Google Scholar
  9. Shaowei Cai, Zhong Jie, and Kaile Su. An effective variable selection heuristic in sls for weighted max-2-sat. Journal of Heuristics, 21(3):433-456, 2015. Google Scholar
  10. Shaowei Cai, Chuan Luo, John Thornton, and Kaile Su. Tailoring local search for partial maxsat. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, AAAI’14, page 2623–2629. AAAI Press, 2014. Google Scholar
  11. Shaowei Cai and Kaile Su. Local search with configuration checking for sat. In 2011 IEEE 23rd International Conference on Tools with Artificial Intelligence, pages 59-66. IEEE, 2011. Google Scholar
  12. Shaowei Cai and Kaile Su. Local search for boolean satisfiability with configuration checking and subscore. Artificial Intelligence, 204:75-98, 2013. Google Scholar
  13. Byungki Cha, Kazuo Iwama, Yahiko Kambayashi, and Shuichi Miyazaki. Local search algorithms for partial maxsat. In Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Conference on Innovative Applications of Artificial Intelligence, AAAI’97/IAAI’97, page 263–268. AAAI Press, 1997. Google Scholar
  14. Ruiwen Chen and Rahul Santhanam. Improved algorithms for sparse max-sat and max-k-csp. In Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT 2015), pages 33-45. Springer, 2015. Google Scholar
  15. Vašek Chvátal and Bruce Reed. Mick gets some (the odds are on his side) [satisfiability]. In Proceedings of the 33rd Annual Symposium on Foundations of Computer Science, pages 620-627. IEEE, 1992. Google Scholar
  16. Amin Coja-Oghlan. The asymptotic k-sat threshold. In Proceedings of the 46th Annual ACM Symposium on Theory of Computing, pages 804-813. ACM, 2014. Google Scholar
  17. Don Coppersmith, David Gamarnik, MohammadTaghi Hajiaghayi, and Gregory B Sorkin. Random max sat, random max cut, and their phase transitions. Random Structures & Algorithms, 24(4):502-545, 2004. Google Scholar
  18. Kevin P Costello, Asaf Shapira, and Prasad Tetali. Randomized greedy: new variants of some classic approximation algorithms. In Proceedings of the twenty-second annual ACM-SIAM symposium on Discrete Algorithms, pages 647-655. Society for Industrial and Applied Mathematics, 2011. Google Scholar
  19. Jessica Davies and Fahiem Bacchus. Solving maxsat by solving a sequence of simpler sat instances. In Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming, pages 225-239. Springer, 2011. Google Scholar
  20. Pieter-Tjerk de Boer, Dirk P Kroese, Shie Mannor, and Reuven Y Rubinstein. A tutorial on the cross-entropy method. Annals of Operations Research, 134(1):19-67, 2005. Google Scholar
  21. Jian Ding, Allan Sly, and Nike Sun. Proof of the satisfiability conjecture for large k. In Proceedings of the forty-seventh annual ACM symposium on Theory of computing, pages 59-68, 2015. Google Scholar
  22. Ding-Zhu Du, Jun Gu, and Panos M. Pardalos, editors. Satisfiability Problem: Theory and Applications, Proceedings of a DIMACS Workshop, Piscataway, New Jersey, USA, March 11-13, 1996, volume 35 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. DIMACS/AMS, 1997. Google Scholar
  23. Paul Erdős and John L Selfridge. On a combinatorial game. Journal of Combinatorial Theory, Series A, 14(3):298-301, 1973. Google Scholar
  24. Paola Festa, Panos M Pardalos, Leonidas S Pitsoulis, and Mauricio GC Resende. Grasp with path-relinking for the weighted maximum satisfiability problem. In International Workshop on Experimental and Efficient Algorithms, pages 367-379. Springer, 2005. Google Scholar
  25. Ehud Friedgut and Jean Bourgain. Sharp thresholds of graph properties, and the k-sat problem. Journal of the American Mathematical Society, 12(4):1017-1054, 1999. Google Scholar
  26. Gregory Gutin and Abraham P Punnen. The Traveling Salesman Problem and Its Variations, volume 12. Springer Science & Business Media, 2006. Google Scholar
  27. Gregory Gutin and Anders Yeo. Polynomial approximation algorithms for the tsp and the qap with a factorial domination number. Discrete Applied Mathematics, 119(1-2):107-116, 2002. Google Scholar
  28. Johan Håstad. Some optimal inapproximability results. Journal of the ACM (JACM), 48(4):798-859, 2001. Google Scholar
  29. Federico Heras, Javier Larrosa, and Albert Oliveras. Minimaxsat: An efficient weighted max-sat solver. Journal of Artificial Intelligence Research (JAIR), 31:1-32, 2008. Google Scholar
  30. Holger H Hoos and Thomas Stützle. Stochastic Local Search: Foundations and Applications. Elsevier, 2004. Google Scholar
  31. Chu Min Li and Felip Manyà. MaxSAT, hard and soft constraints, volume 185, pages 613-631. IOS Press, 2009. Google Scholar
  32. Cheng Luo, Shanyong Cai, Wenchuan Wu, Zhong Jie, and Kuan-Wu Su. Ccls: An efficient local search algorithm for weighted maximum satisfiability. IEEE Transactions on Computers, 64(7):1830-1843, 2014. Google Scholar
  33. Chuan Luo, Shaowei Cai, Kaile Su, and Wei Wu. Clause states based configuration checking in local search for satisfiability. IEEE transactions on Cybernetics, 45(5):1028-1041, 2014. Google Scholar
  34. Chuan Luo, Shaowei Cai, Wei Wu, and Kaile Su. Focused random walk with configuration checking and break minimum for satisfiability. In International Conference on Principles and Practice of Constraint Programming, pages 481-496. Springer, 2013. Google Scholar
  35. Stephan Mertens, Marc Mézard, and Riccardo Zecchina. Threshold values of random k-sat from the cavity method. Random Structures & Algorithms, 28(3):340-373, 2006. Google Scholar
  36. Patrick Mills and Edward Tsang. Guided local search for solving sat and weighted max-sat problems. Journal of Automated Reasoning, 24(1-2):205-223, 2000. Google Scholar
  37. Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided maxsat resolution. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, pages 2717-2723. AAAI Press, 2014. Google Scholar
  38. Denis Pankratov and Allan Borodin. On the relative merits of simple local search methods for the max-sat problem. In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), SAT’10, page 223–236, Berlin, Heidelberg, 2010. Springer-Verlag. Google Scholar
  39. Matthias Poloczek. Bounds on greedy algorithms for max sat. In Proceedings of the 19th European Conference on Algorithms, ESA’11, page 37–48, Berlin, Heidelberg, 2011. Springer-Verlag. Google Scholar
  40. Matthias Poloczek, Georg Schnitger, David P Williamson, and Anke Van Zuylen. Greedy algorithms for the maximum satisfiability problem: Simple algorithms and inapproximability bounds. SIAM Journal on Computing, 46(3):1029-1061, 2017. Google Scholar
  41. Matthias Poloczek and David P Williamson. An experimental evaluation of fast approximation algorithms for the maximum satisfiability problem. In International Symposium on Experimental Algorithms, pages 246-261. Springer, 2016. Google Scholar
  42. Bart Selman, Henry A. Kautz, and Bram Cohen. Noise strategies for improving local search. In Proceedings of the Twelfth National Conference on Artificial Intelligence (Vol. 1), page 337–343. American Association for Artificial Intelligence, 1994. Google Scholar
  43. Bart Selman, Henry A. Kautz, and Bram Cohen. Local search strategies for satisfiability testing. In DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 521-532, 1996. Google Scholar
  44. Bart Selman, Hector Levesque, and David Mitchell. A new method for solving hard satisfiability problems. In Proceedings of the Tenth National Conference on Artificial Intelligence, pages 440-446. AAAI Press, 1992. Google Scholar
  45. Kevin Smyth, Holger H Hoos, and Thomas Stützle. Iterated robust tabu search for max-sat. In Conference of the Canadian Society for Computational Studies of Intelligence, pages 129-144. Springer, 2003. Google Scholar
  46. Sun grid engine (sge) quickstart. URL: http://star.mit.edu/cluster/docs/0.93.3/guides/sge.html.
  47. Mihalis Yannakakis. On the approximation of maximum satisfiability. Journal of Algorithms, 17(3):475-502, 1994. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact