Document Open Access Logo

ParLS-PBO: A Parallel Local Search Solver for Pseudo Boolean Optimization

Authors Zhihan Chen , Peng Lin , Hao Hu , Shaowei Cai

PDF
Thumbnail PDF

File

LIPIcs.CP.2024.5.pdf
  • Filesize: 0.98 MB
  • 17 pages

Document Identifiers

Author Details

Zhihan Chen
  • Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
  • School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing, China
Peng Lin
  • Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
  • School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing, China
Hao Hu
  • Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
Shaowei Cai
  • Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
  • School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing, China

Funding

This work is supported by National Key R&D Program of China (2023YFA1009500).

Cite AsGet BibTex

Zhihan Chen, Peng Lin, Hao Hu, and Shaowei Cai. ParLS-PBO: A Parallel Local Search Solver for Pseudo Boolean Optimization. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CP.2024.5

Abstract

As a broadly applied technique in numerous optimization problems, recently, local search has been employed to solve Pseudo-Boolean Optimization (PBO) problem. A representative local search solver for PBO is LS-PBO. In this paper, firstly, we improve LS-PBO by a dynamic scoring mechanism, which dynamically strikes a balance between score on hard constraints and score on the objective function. Moreover, on top of this improved LS-PBO, we develop the first parallel local search PBO solver. The main idea is to share good solutions among different threads to guide the search, by maintaining a pool of feasible solutions. For evaluating solutions when updating the pool, we propose a function that considers both the solution quality and the diversity of the pool. Furthermore, we calculate the polarity density in the pool to enhance the scoring function of local search. Our empirical experiments show clear benefits of the proposed parallel approach, making it competitive with the parallel version of the famous commercial solver Gurobi.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Parallel algorithms
  • Theory of computation → Randomized local search
Keywords
  • Pseudo-Boolean Optimization
  • Parallel Solving
  • Local Search
  • Scoring Function
  • Solution Pool

Metrics

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

Supplementary Materials

References

  1. Adrian Balint and Uwe Schöning. Choosing probability distributions for stochastic local search and the role of make versus break. In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, volume 7317 of Lecture Notes in Computer Science, pages 16-29. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_3.
  2. Peter Barth. A davis-putnam based enumeration algorithm for linear pseudo-boolean optimization. Technical report, Max Plank Institute for Computer Science, 1995. Google Scholar
  3. Belaid Benhamou, Lakhdar Sais, and Pierre Siegel. Two proof procedures for a cardinality based language in propositional calculus. In Patrice Enjalbert, Ernst W. Mayr, and Klaus W. Wagner, editors, STACS 94, 11th Annual Symposium on Theoretical Aspects of Computer Science, Caen, France, February 24-26, 1994, Proceedings, volume 775 of Lecture Notes in Computer Science, pages 71-82. Springer, 1994. URL: https://doi.org/10.1007/3-540-57785-8_132.
  4. Jeremias Berg, Emilia Oikarinen, Matti Järvisalo, and Kai Puolamäki. Minimum-width confidence bands via constraint optimization. In International Conference on Principles and Practice of Constraint Programming, pages 443-459. Springer, 2017. Google Scholar
  5. Ksenia Bestuzheva, Mathieu Besançon, Wei-Kun Chen, Antonia Chmiela, Tim Donkiewicz, Jasper van Doornmalen, Leon Eifler, Oliver Gaul, Gerald Gamrath, Ambros Gleixner, et al. The scip optimization suite 8.0. arXiv preprint arXiv:2112.08872, 2021. Google Scholar
  6. Shaowei Cai, Chuan Luo, and Kaile Su. Ccanr: A configuration checking based local search solver for non-random satisfiability. In Marijn Heule and Sean A. Weaver, editors, Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, volume 9340 of Lecture Notes in Computer Science, pages 1-8. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_1.
  7. Yuning Chen and Jin-Kao Hao. Memetic search for the generalized quadratic multiple knapsack problem. IEEE Trans. Evol. Comput., 20(6):908-923, 2016. URL: https://doi.org/10.1109/TEVC.2016.2546340.
  8. Zhihan Chen, Xindi Zhang, Yuhang Qian, and Shaowei Cai. Prs: A new parallel/distributed framework for sat. SAT COMPETITION 2023, page 39, 2023. Google Scholar
  9. 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. URL: https://ojs.aaai.org/index.php/AAAI/article/view/25505, URL: https://doi.org/10.1609/AAAI.V37I4.25505.
  10. Yi Chu, Shaowei Cai, Chuan Luo, Zhendong Lei, and Cong Peng. Towards more efficient local search for pseudo-boolean optimization. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Schloss-Dagstuhl-Leibniz Zentrum für Informatik, 2023. Google Scholar
  11. Olivier Coudert and Jean Christophe Madre. New ideas for solving covering problems. In Bryan Preas, editor, Proceedings of the 32st Conference on Design Automation, San Francisco, California, USA, Moscone Center, June 12-16, 1995, pages 641-646. ACM Press, 1995. URL: https://doi.org/10.1145/217474.217603.
  12. Jo Devriendt, Stephan Gocht, Emir Demirovic, Jakob Nordström, and Peter J. Stuckey. Cutting to the core of pseudo-boolean optimization: Combining core-guided search with cutting planes reasoning. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 3750-3758. AAAI Press, 2021. URL: https://ojs.aaai.org/index.php/AAAI/article/view/16492, URL: https://doi.org/10.1609/AAAI.V35I5.16492.
  13. Niklas Eén and Niklas Sörensson. Translating pseudo-boolean constraints into sat. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):1-26, 2006. Google Scholar
  14. Jan Elffers and Jakob Nordström. Divide and conquer: Towards faster pseudo-boolean solving. In Jérôme Lang, editor, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 1291-1299. ijcai.org, 2018. Google Scholar
  15. Armin Biere Katalin Fazekas Mathias Fleury and Maximilian Heisinger. Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020. SAT COMPETITION, 2020:50, 2020. Google Scholar
  16. Ludovic Le Frioux, Souheib Baarir, Julien Sopena, and Fabrice Kordon. Painless: A framework for parallel SAT solving. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 233-250. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_15.
  17. LLC Gurobi Optimization. Gurobi optimizer reference manual, 2021. Google Scholar
  18. Markus Iser, Jeremias Berg, and Matti Järvisalo. Oracle-based local search for pseudo-boolean optimization. In Kobi Gal, Ann Nowé, Grzegorz J. Nalepa, Roy Fairstein, and Roxana Radulescu, editors, ECAI 2023 - 26th European Conference on Artificial Intelligence, September 30 - October 4, 2023, Kraków, Poland - Including 12th Conference on Prestigious Applications of Intelligent Systems (PAIS 2023), volume 372 of Frontiers in Artificial Intelligence and Applications, pages 1124-1131. IOS Press, 2023. URL: https://doi.org/10.3233/FAIA230387.
  19. Luyu Jiang, Dantong Ouyang, Qi Zhang, and Liming Zhang. Decils-pbo: an effective local search method for pseudo-boolean optimization. CoRR, abs/2301.12251, 2023. URL: https://doi.org/10.48550/arXiv.2301.12251.
  20. Gergely Kovásznai, Balázs Erdélyi, and Csaba Biró. Investigations of graph properties in terms of wireless sensor network optimization. In 2018 IEEE International Conference on Future IoT Technologies (Future IoT), pages 1-8. IEEE, 2018. Google Scholar
  21. Gergely Kovásznai, Krisztián Gajdár, and Laura Kovács. Portfolio sat and smt solving of cardinality constraints in sensor network optimization. In 2019 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pages 85-91. IEEE, 2019. Google Scholar
  22. Daniel Le Berre and Anne Parrain. The sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation, 7(2-3):59-64, 2010. Google Scholar
  23. Zhendong Lei and Shaowei Cai. Solving (weighted) partial maxsat by dynamic local search for SAT. In Jérôme Lang, editor, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 1346-1352. ijcai.org, 2018. URL: https://doi.org/10.24963/ijcai.2018/187.
  24. 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. URL: https://doi.org/10.1007/978-3-030-80223-3_23.
  25. Chu Min Li and Yu Li. Satisfying versus falsifying in local search for satisfiability - (poster presentation). In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, volume 7317 of Lecture Notes in Computer Science, pages 477-478. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_43.
  26. Stan Y. Liao and Srinivas Devadas. Solving covering problems using lpr-based lower bounds. In Ellen J. Yoffa, Giovanni De Micheli, and Jan M. Rabaey, editors, Proceedings of the 34st Conference on Design Automation, Anaheim, California, USA, Anaheim Convention Center, June 9-13, 1997, pages 117-120. ACM Press, 1997. URL: https://doi.org/10.1145/266021.266046.
  27. Marius Lindauer, Katharina Eggensperger, Matthias Feurer, André Biedenkapp, Difan Deng, Carolin Benjamins, Tim Ruhkopf, René Sass, and Frank Hutter. Smac3: A versatile bayesian optimization package for hyperparameter optimization. Journal of Machine Learning Research, 23(54):1-9, 2022. Google Scholar
  28. Joao Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning sat solvers. In Handbook of satisfiability, pages 133-182. IOS Press, 2021. Google Scholar
  29. Ruben Martins, Vasco Manquinho, and Inês Lynce. Exploiting cardinality encodings in parallel maximum satisfiability. In 2011 IEEE 23rd International Conference on Tools with Artificial Intelligence, pages 313-320. IEEE, 2011. Google Scholar
  30. Ruben Martins, Vasco Manquinho, and Inês Lynce. Parallel search for maximum satisfiability. AI Communications, 25(2):75-95, 2012. Google Scholar
  31. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Open-wbo: A modular maxsat solver,. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 438-445. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_33.
  32. Ruben Martins and Justine Sherry. Lisbon wedding: seating arrangements using maxsat. MaxSAT Evaluation, pages 25-26, 2017. Google Scholar
  33. Olivier Roussel and Vasco M. Manquinho. Pseudo-boolean and cardinality constraints. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1087-1129. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201012.
  34. Yuji Shinano, Stefan Heinz, Stefan Vigerske, and Michael Winkler. Fiberscip - A shared memory parallelization of SCIP. INFORMS J. Comput., 30(1):11-30, 2018. URL: https://doi.org/10.1287/ijoc.2017.0762.
  35. Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. Improvements to the implicit hitting set approach to pseudo-boolean optimization. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 13:1-13:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.13.
  36. Rodrigue Konan Tchinda and Clémentin Tayou Djamegni. Hkis, hcad, pakis and painless exmaplelcmdistchronobt in the sc21. SAT COMPETITION, 2021:26, 2021. 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