Document Open Access Logo

Deep Cooperation of Local Search and Unit Propagation Techniques

Authors Xiamin Chen , Zhendong Lei , Pinyan Lu

PDF
Thumbnail PDF

File

LIPIcs.CP.2024.6.pdf
  • Filesize: 1.41 MB
  • 16 pages

Document Identifiers

Author Details

Xiamin Chen
  • Shanghai University of Finance and Economics, China
Zhendong Lei
  • Huawei Taylor Lab, Shanghai, China
Pinyan Lu
  • Shanghai University of Finance and Economics, Shanghai, China
  • Huawei Taylor Lab, Shanghai, China

Funding

  • Lu, Pinyan: National Key R&D Program of China (2023YFA1009500).

Cite AsGet BibTex

Xiamin Chen, Zhendong Lei, and Pinyan Lu. Deep Cooperation of Local Search and Unit Propagation Techniques. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CP.2024.6

Abstract

Local search (LS) is an efficient method for solving combinatorial optimization problems such as MaxSAT and Pseudo Boolean Problems (PBO). However, due to a lack of reasoning power and global information, LS methods get stuck at local optima easily. In contrast to the LS, Systematic Search utilizes unit propagation and clause learning techniques with strong reasoning capabilities to avoid falling into local optima. Nevertheless, the complete search is generally time-consuming to obtain a global optimal solution. This work proposes a deep cooperation framework combining local search and unit propagation to address their inherent disadvantages. First, we design a mechanism to detect when LS gets stuck, and then a well-designed unit propagation procedure is called upon to help escape the local optima. To the best of our knowledge, we are the first to integrate unit propagation technique within LS to overcome local optima. Experiments based on a broad range of benchmarks from MaxSAT Evaluations, PBO competitions, the Mixed Integer Programming Library, and three real-life cases validate that our method significantly improves three state-of-the-art MaxSAT and PBO local search solvers.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorial optimization
Keywords
  • PBO
  • Partial MaxSAT
  • LS
  • CDCL

Metrics

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

References

  1. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. SAT-based MaxSAT algorithms. Artif. Intell., 196:77-105, 2013. Google Scholar
  2. Carlos Ansótegui and Joel Gabàs. WPM3: an (in)complete algorithm for weighted partial maxsat. Artif. Intell., 250:37-57, 2017. Google Scholar
  3. Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, and Lakhdar Sais. Boosting local search thanks to cdcl. In Christian G. Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, volume 6397 of Lecture Notes in Computer Science, pages 474-488. Springer, 2010. Google Scholar
  4. Adrian Balint, Michael Henn, and Oliver Gableske. A novel approach to combine a sls-and a dpll-solver for the satisfiability problem. In Theory and Applications of Satisfiability Testing-SAT 2009: 12th International Conference, SAT 2009, Swansea, UK, June 30-July 3, 2009. Proceedings 12, pages 284-297. Springer, 2009. Google Scholar
  5. Jeremias Berg, Emir Demirovic, and Peter J. Stuckey. Core-boosted linear search for incomplete maxsat. In Louis-Martin Rousseau and Kostas Stergiou, editors, Proceedings CPAIOR 2019,, volume 11494, pages 39-56, 2019. Google Scholar
  6. Daniel Le Berre and Anne Parrain. The sat4j library, release 2.2. JSAT, 7(2-3):59-64, 2010. Google Scholar
  7. Shaowei Cai and Zhendong Lei. Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability. Artif. Intell., 287:103354, 2020. Google Scholar
  8. Shaowei Cai, Chuan Luo, John Thornton, and Kaile Su. Tailoring local search for partial MaxSAT. In Proceedings of AAAI 2014, pages 2623-2629, 2014. Google Scholar
  9. Shaowei Cai and Xindi Zhang. Deep cooperation of CDCL and local search for SAT (extended abstract). In Luc De Raedt, editor, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022, pages 5274-5278. ijcai.org, 2022. Google Scholar
  10. Donald Chai and Andreas Kuehlmann. A fast pseudo-Boolean constraint solver. IEEE Trans. on CAD of Integrated Circuits and Systems, 24(3):305-317, 2005. Google Scholar
  11. Yi Chu, Shaowei Cai, and Chuan Luo. Nuwls: Improving local search for (weighted) partial maxsat by new weighting techniques. In Brian Williams, Yiling Chen, and Jennifer Neville, editors, Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, pages 3915-3923. AAAI Press, 2023. Google Scholar
  12. Yi Chu, Shaowei Cai, Chuan Luo, Zhendong Lei, and Cong Peng. Towards more efficient local search for pseudo-boolean optimization. In Roland H. C. Yap, editor, 29th International Conference on Principles and Practice of Constraint Programming, CP 2023, August 27-31, 2023, Toronto, Canada, volume 280 of LIPIcs, pages 12:1-12:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  13. James M Crawford. Solving satisfiability problems using a combination of systematic and local search. In Second DIMACS Challenge: cliques, coloring, and satisfiability. Citeseer, 1993. Google Scholar
  14. Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Proceedings of CP 2011, pages 225-239, 2011. Google Scholar
  15. Emir Demirovic and Peter J. Stuckey. Techniques inspired by local search for incomplete maxsat and the linear algorithm: Varying resolution and solution-guided search. In Thomas Schiex and Simon de Givry, editors, Proceedings of CP 2019, volume 11802, pages 177-194, 2019. Google Scholar
  16. Jo Devriendt, Stephan Gocht, Emir Demirović, Peter Stuckey, and Jakob Nordström. Cutting to the core of pseudo-Boolean optimization: Combining core-guided search with cutting planes reasoning. In AAAI 2021,Accepted, 2021. URL: http://www.csc.kth.se/~jakobn/research/CuttingToTheCore_AAAI.pdf.
  17. Jan Elffers, Jesús Giráldez-Cru, Jakob Nordström, and Marc Vinyals. Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Proceedings of SAT 2018, pages 75-93, 2018. Google Scholar
  18. Jan Elffers and Jakob Nordström. Divide and conquer: Towards faster pseudo-Boolean solving. In Jérôme Lang, editor, Proceedings of IJCAI 2018, pages 1291-1299, 2018. Google Scholar
  19. Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121 of Lecture Notes in Computer Science, pages 252-265. Springer, 2006. Google Scholar
  20. Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In Proceedings of SAT 2006, pages 252-265, 2006. Google Scholar
  21. Djamal Habet, Chu Min Li, Laure Devendeville, and Michel Vasquez. A hybrid approach for sat. In International Conference on Principles and Practice of Constraint Programming, pages 172-184. Springer, 2002. Google Scholar
  22. William S Havens and Bistra N Dilkina. A hybrid schema for systematic local search. In Advances in Artificial Intelligence: 17th Conference of the Canadian Society for Computational Studies of Intelligence, Canadian AI 2004, London, Ontario, Canada, May 17-19, 2004. Proceedings 17, pages 248-260. Springer, 2004. Google Scholar
  23. Saurabh Joshi, Prateek Kumar, Sukrut Rao, and Ruben Martins. Open-wbo-inc: Approximation strategies for incomplete weighted maxsat. J. Satisf. Boolean Model. Comput., 11(1):73-97, 2019. Google Scholar
  24. Narendra Jussien and Olivier Lhomme. Local search with constraint propagation and conflict-based heuristics. Artificial Intelligence, 139(1):21-45, 2002. Google Scholar
  25. Tuukka Korhonen, Jeremias Berg, Paul Saikko, and Matti Järvisalo. Maxpre: an extended maxsat preprocessor. In International Conference on Theory and Applications of Satisfiability Testing, pages 449-456. Springer, 2017. Google Scholar
  26. Zhendong Lei and Shaowei Cai. Solving (weighted) partial maxsat by dynamic local search for SAT. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden., pages 1346-1352, 2018. Google Scholar
  27. Zhendong Lei, Shaowei Cai, Chuan Luo, and Holger H. Hoos. Efficient local search for pseudo boolean optimization. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 332-348. Springer, 2021. Google Scholar
  28. Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining clause learning and branch and bound for maxsat. In Laurent D. Michel, editor, 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021, volume 210 of LIPIcs, pages 38:1-38:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  29. Jan-Hendrik Lorenz and Florian Wörz. On the effect of learned clauses on stochastic local search. In Theory and Applications of Satisfiability Testing-SAT 2020: 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings 23, pages 89-106. Springer, 2020. Google Scholar
  30. Bertrand Mazure, Lakhdar Sais, and Éric Grégoire. Boosting complete techniques thanks to local search methods. Annals of mathematics and artificial intelligence, 22:319-331, 1998. Google Scholar
  31. Alexander Nadel. Anytime weighted maxsat with improved polarity selection and bit-vector optimization. In Clark W. Barrett and Jin Yang, editors, Proceedings of FMCAD 2019, pages 193-202, 2019. Google Scholar
  32. Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided MaxSAT resolution. In Proceedings of AAAI 2014, pages 2717-2723, 2014. Google Scholar
  33. Steven Prestwich. Randomised backtracking for linear pseudo-Boolean constraint problems. In Proceedings of CPAIOR 2002, pages 7-20, 2002. Google Scholar
  34. João P. Marques Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiabilitysatlike. In Rob A. Rutenbar and Ralph H. J. M. Otten, editors, Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1996, San Jose, CA, USA, November 10-14, 1996, pages 220-227. IEEE Computer Society / ACM, 1996. Google Scholar
  35. Robert Wille, Hongyan Zhang, and Rolf Drechsler. ATPG for reversible circuits using simulation, boolean satisfiability, and pseudo boolean optimization. In IEEE Computer Society Annual Symposium on VLSI, ISVLSI 2011, 4-6 July 2011, Chennai, India, pages 120-125. IEEE Computer Society, 2011. Google Scholar
  36. Aolong Zha, Miyuki Koshimura, and Hiroshi Fujita. A hybrid encoding of pseudo-Boolean constraints into CNF. In Proceedings of TAAI 2017, pages 9-12. IEEE Computer Society, 2017. Google Scholar
  37. Yuhang Zhang, Richard I. Hartley, John Mashford, and Stewart Burn. Superpixels via pseudo-boolean optimization. In Dimitris N. Metaxas, Long Quan, Alberto Sanfeliu, and Luc Van Gool, editors, IEEE International Conference on Computer Vision, ICCV 2011, Barcelona, Spain, November 6-13, 2011, pages 1387-1394. IEEE Computer Society, 2011. Google Scholar
  38. Jiongzhi Zheng, Kun He, Jianrong Zhou, Yan Jin, Chu-Min Li, and Felip Manyà. Bandmaxsat: A local search maxsat solver with multi-armed bandit. In Luc De Raedt, editor, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022, pages 1901-1907. ijcai.org, 2022. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact