Document Open Access Logo

Towards More Efficient Local Search for Pseudo-Boolean Optimization

Authors Yi Chu , Shaowei Cai , Chuan Luo , Zhendong Lei , Cong Peng

PDF
Thumbnail PDF

File

LIPIcs.CP.2023.12.pdf
  • Filesize: 0.89 MB
  • 18 pages

Document Identifiers

Author Details

Yi Chu
  • Institute of Software, Chinese Academy of Sciences, Beijing, China
Shaowei Cai
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
Chuan Luo
  • School of Software, Beihang University, Beijing, China
Zhendong Lei
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
Cong Peng
  • Finovation in CCBFT, Beijing, China

Funding

This work is supported by the Strategic Priority Research Program of the Chinese Academy of Sciences, Grant No. XDA0320000 and XDA0320300, the National Natural Science Foundation of China under Grant 62302492, and Grant 62202025, the Research Program of CCBFT, Grant No. KT2100040, and CCF-Huawei Populus Grove Fund under Grant CCF-HuaweiSY20231.

Cite AsGet BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CP.2023.12

Abstract

Pseudo-Boolean (PB) constraints are highly expressive, and many combinatorial optimization problems can be modeled using pseudo-Boolean optimization (PBO). It is recognized that stochastic local search (SLS) is a powerful paradigm for solving combinatorial optimization problems, but the development of SLS for solving PBO is still in its infancy. In this paper, we develop an effective SLS algorithm for solving PBO, dubbed NuPBO, which introduces a novel scoring function for PB constraints and a new weighting scheme. We conduct experiments on a broad range of six public benchmarks, including three real-world benchmarks, a benchmark from PB competition, an integer linear programming optimization benchmark, and a crafted combinatorial benchmark, to compare NuPBO against five state-of-the-art competitors, including a recently-proposed SLS PBO solver LS-PBO, two complete PB solvers PBO-IHS and RoundingSat, and two mixed integer programming (MIP) solvers Gurobi and SCIP. NuPBO has been exhibited to perform best on these three real-world benchmarks. On the other three benchmarks, NuPBO shows competitive performance compared to state-of-the-art competitors, and it significantly outperforms LS-PBO, indicating that NuPBO greatly advances the state of the art in SLS for solving PBO.

Subject Classification

ACM Subject Classification
  • Theory of computation → Randomized local search
Keywords
  • Pseudo-Boolean Optimization
  • Stochastic Local Search
  • Scoring Function
  • Weighting Scheme

Metrics

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

Supplementary Materials

References

  1. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. SAT-based MaxSAT algorithms. Artificial Intelligence, 196:77-105, 2013. Google Scholar
  2. Carlos Ansótegui and Joel Gabàs. WPM3: An (in)complete algorithm for weighted partial MaxSAT. Artificial Intelligence, 250:37-57, 2017. Google Scholar
  3. VL Beresnev, EN Goncharov, and AA Mel’nikov. Local search with a generalized neighborhood in the optimization problem for pseudo-boolean functions. Journal of Applied and Industrial Mathematics, 6:22-30, 2012. Google Scholar
  4. Jeremias Berg, Emir Demirovic, and Peter J. Stuckey. Core-boosted linear search for incomplete MaxSAT. In Proceedings of CPAIOR 2019, pages 39-56, 2019. Google Scholar
  5. Shaowei Cai and Zhendong Lei. Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability. Artificial Intelligence, 287:103354, 2020. Google Scholar
  6. Shaowei Cai, Chuan Luo, Jinkun Lin, and Kaile Su. New local search methods for partial MaxSAT. Artificial Intelligence, 240:1-18, 2016. Google Scholar
  7. Shaowei Cai, Chuan Luo, and Kaile Su. Scoring functions based on second level score for k-sat with long clauses. J. Artif. Intell. Res., 51:413-441, 2014. URL: https://doi.org/10.1613/jair.4480.
  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. Byungki Cha and Kazuo Iwama. Performance test of local search algorithms using new types of random CNF formulas. In Proceedings of IJCAI 1995, pages 304-311, 1995. Google Scholar
  10. Byungki Cha, Kazuo Iwama, Yahiko Kambayashi, and Shuichi Miyazaki. Local search algorithms for partial MAXSAT. In Proceedings of AAAI 1997, pages 263-268, 1997. Google Scholar
  11. 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
  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 Proceedings of AAAI 2021, pages 3750-3758, 2021. Google Scholar
  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 IJCAI 2018, pages 1291-1299, 2018. Google Scholar
  15. Jan Elffers and Jakob Nordström. A cardinal improvement to pseudo-Boolean solving. In Proceedings of AAAI 2020, pages 1495-1503, 2020. Google Scholar
  16. Gerald Gamrath, Daniel Anderson, Ksenia Bestuzheva, Wei-Kun Chen, Leon Eifler, Maxime Gasse, Patrick Gemander, Ambros Gleixner, Leona Gottwald, Katrin Halbig, Gregor Hendel, Christopher Hojny, Thorsten Koch, Pierre Le Bodic, Stephen J. Maher, Frederic Matter, Matthias Miltenberger, Erik Mühmer, Benjamin Müller, Marc E. Pfetsch, Franziska Schlösser, Felipe Serrano, Yuji Shinano, Christine Tawfik, Stefan Vigerske, Fabian Wegscheider, Dieter Weninger, and Jakob Witzig. The SCIP Optimization Suite 7.0. Technical report, Optimization Online, March 2020. URL: http://www.optimization-online.org/DB_HTML/2020/03/7705.html.
  17. Martin Gebser, Benjamin Kaufmann, and Torsten Schaub. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence, 187:52-89, 2012. Google Scholar
  18. Corrado Gini. Concentration and dependency ratios. Rivista di politica economica, pages 769-792, 1997. Google Scholar
  19. Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2021. URL: https://www.gurobi.com.
  20. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. Google Scholar
  21. Pascal Van Hentenryck and Laurent Michel. Constraint-based local search. The MIT press, 2009. Google Scholar
  22. Holger H. Hoos, Laetitia Jourdan, Marie-Eléonore Kessaci, Thomas Stützle, and Nadarajen Veerapen. Special issue on "stochastic local search: Recent developments and trends". International Transactions in Operational Research, 27(1):697-698, 2020. Google Scholar
  23. Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa. QMaxSAT: A partial Max-SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 8(1-2):95-100, 2012. Google Scholar
  24. 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
  25. Zhendong Lei and Shaowei Cai. Solving (weighted) partial MaxSAT by dynamic local search for SAT. In Proceedings of IJCAI 2018, pages 1346-1352, 2018. Google Scholar
  26. Zhendong Lei, Shaowei Cai, Chuan Luo, and Holger H. Hoos. Efficient local search for pseudo boolean optimization. In Proceedings of SAT 2021, pages 332-348, 2021. Google Scholar
  27. Chuan Luo, Shaowei Cai, Kaile Su, and Wenxuan Huang. CCEHC: An efficient local search algorithm for weighted partial maximum satisfiability. Artificial Intelligence, 243:26-44, 2017. Google Scholar
  28. Chuan Luo, Shaowei Cai, Wei Wu, Zhong Jie, and Kaile Su. CCLS: An efficient local search algorithm for weighted maximum satisfiability. IEEE Transactions on Computers, 64(7):1830-1843, 2015. Google Scholar
  29. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Open-WBO: A modular maxsat solver,. In Proceedings of SAT 2014, pages 438-445, 2014. Google Scholar
  30. Rafiq Muhammad and Peter J. Stuckey. A stochastic non-CNF SAT solver. In Proceedings of PRICAI 2006, pages 120-129, 2006. Google Scholar
  31. Alexander Nadel. Anytime weighted MaxSAT with improved polarity selection and bit-vector optimization. In 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. Olivier Roussel and Vasco Manquinho. Pseudo-boolean and cardinality constraints. In Handbook of satisfiability, pages 1087-1129. IOS Press, 2021. Google Scholar
  34. Masahiko Sakai and Hidetomo Nabeshima. Construction of an ROBDD for a PB-constraint in band form and related techniques for pb-solvers. IEICE Transactions on Information & Systems, 98-D(6):1121-1127, 2015. Google Scholar
  35. Bart Selman and Henry Kautz. Domain-independent extensions to GSAT: solving large structured satisfiability problems. In Proceedings of IJCAI 1993, pages 290-295, 1993. Google Scholar
  36. Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. Pseudo-boolean optimization by implicit hitting sets. In Proceedings of CP 2021, pages 51:1-51:20, 2021. Google Scholar
  37. Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. Improvements to the implicit hitting set approach to pseudo-boolean optimization. In Proceedings of SAT 2022, pages 13:1-13:18, 2022. Google Scholar
  38. John Thornton and Abdul Sattar. Dynamic constraint weighting for over-constrained problems. In Proceedings of PRICAI 1998, pages 377-388, 1998. Google Scholar
  39. Renato Tinós, Michal W Przewozniczek, and Darrell Whitley. Iterated local search with perturbation based on variables interaction for pseudo-boolean optimization. In Proceedings of GECCO 2022, pages 296-304, 2022. Google Scholar
  40. Chris Voudouris and Edward Tsang. Partial constraint satisfaction problems and guided local search. Proc., Practical Application of Constraint Technology (PACT'96), London, pages 337-356, 1996. Google Scholar
  41. Christos Voudouris, Edward PK Tsang, and Abdullah Alsheddy. Guided local search. In Handbook of metaheuristics, pages 321-361. Springer, 2010. Google Scholar
  42. Joachim P. Walser. Solving linear pseudo-boolean constraint problems with local search. In Proceedings of AAAI 1997, pages 269-274, 1997. Google Scholar
  43. Robert Wille, Hongyan Zhang, and Rolf Drechsler. ATPG for reversible circuits using simulation, boolean satisfiability, and pseudo boolean optimization. In Proceedings of ISVLSI 2011, pages 120-125, 2011. Google Scholar
  44. Yuhang Zhang, Richard Hartley, John Mashford, and Stewart Burn. Superpixels via pseudo-boolean optimization. In Proceedings of ICCV 2011, pages 1387-1394, 2011. Google Scholar
  45. Jiongzhi Zheng, Kun He, Jianrong Zhou, Yan Jin, Chu-Min Li, and Felip Manya. BandMaxSAT: A local search maxsat solver with multi-armed bandit. In Proceedings of IJCAI 2022, pages 1901-1907, 2022. 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