Document Open Access Logo

Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets

Authors Hannes Ihalainen , Jeremias Berg , Matti Järvisalo , Bart Bogaerts

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CP.2025.15.pdf
  • Filesize: 1.15 MB
  • 26 pages
HTML5 Logo HTML (experimental)
LIPIcs.CP.2025.15.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorial optimization
  • Theory of computation → Constraint and logic programming
Keywords
  • Implicit hitting sets
  • symmetries
  • unsatisfiable cores
  • pseudo-Boolean optimization

Metrics

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

Abstract

We propose symmetric core learning (SCL) as a novel approach to making the implicit hitting set approach (IHS) to constraint optimization more symmetry-aware. SCL has the potential of significantly reducing the number of iterations and, in particular, the number of calls to an NP decision solver for extracting individual unsatisfiable cores. As the technique is focused on generating symmetric cores to the hitting set component of IHS, SCL is generally applicable in IHS-style search for essentially any constraint optimization paradigm. In this work, we focus in particular on integrating SCL to IHS for pseudo-Boolean optimization (PBO), as earlier proposed static symmetry breaking through lex-leader constraints generated before search turns out to often degrade the performance of the IHS approach to PBO. In contrast, we show that SCL can improve the runtime performance of a state-of-the-art IHS approach to PBO and generally does not impose significant overhead in terms of runtime performance.

Cite As Get BibTex

Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts. Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 15:1-15:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CP.2025.15

Author Details

Hannes Ihalainen
  • University of Helsinki, Finland
Jeremias Berg
  • University of Helsinki, Finland
Matti Järvisalo
  • University of Helsinki, Finland
Bart Bogaerts
  • KU Leuven, Belgium
  • Vrije Universiteit Brussel, Belgium

Funding

  • Ihalainen, Hannes: Partially funded by Research Council of Finland under grant 356046.
  • Berg, Jeremias: Research Council of Finland under grant 362987.
  • Järvisalo, Matti: Partially funded by Research Council of Finland under grant 356046.
  • Bogaerts, Bart: Partially funded by Fonds Wetenschappelijk Onderzoek - Vlaanderen (project G064925N) and by the European Union (ERC, CertiFOX, 101122653). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

Supplementary Materials

References

  1. Fadi A. Aloul, Arathi Ramani, Igor L. Markov, and Karem A. Sakallah. ShatterPB: symmetry-breaking for pseudo-Boolean formulas. In Masaharu Imai, editor, Proceedings of the 2004 Conference on Asia South Pacific Design Automation: Electronic Design and Solution Fair 2004, Yokohama, Japan, January 27-30, 2004, pages 883-886. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/ASPDAC.2004.179.
  2. Fadi A. Aloul, Karem A. Sakallah, and Igor L. Markov. Efficient symmetry breaking for Boolean satisfiability. IEEE Trans. Computers, 55(5):549-558, 2006. URL: https://doi.org/10.1109/TC.2006.75.
  3. Markus Anders, Sofia Brenner, and Gaurav Rattan. satsuma: Structure-based symmetry breaking in SAT. In Supratik Chakraborty and Jie-Hong Roland Jiang, editors, 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, 2024, Pune, India, volume 305 of LIPIcs, pages 4:1-4:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.SAT.2024.4.
  4. Markus Anders, Pascal Schweitzer, and Mate Soos. Algorithms transcending the SAT-symmetry interface. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 1:1-1:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.1.
  5. Fahiem Bacchus, Antti Hyttinen, Matti Järvisalo, and Paul Saikko. Reduced cost fixing in MaxSAT. In J. Christopher Beck, editor, Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10416 of Lecture Notes in Computer Science, pages 641-651. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_41.
  6. Belaid Benhamou, Tarek Nabhani, Richard Ostrowski, and Mohamed Réda Saïdi. Enhancing clause learning by symmetry in SAT solvers. In 22nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2010, Arras, France, 27-29 October 2010 - Volume 1, pages 329-335. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/ICTAI.2010.55.
  7. Jeremias Berg, Fahiem Bacchus, and Alex Poole. Abstract cores in implicit hitting set MaxSAT solving. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 277-294. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_20.
  8. Jeremias Berg and Matti Järvisalo. Weight-aware core extraction in SAT-based MaxSAT solving. In J. Christopher Beck, editor, Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10416 of Lecture Notes in Computer Science, pages 652-670. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_42.
  9. Ignace Bleukx, Hélène Verhaeghe, Bart Bogaerts, and Tias Guns. Exploiting symmetries in MUS computation. In Toby Walsh, Julie Shah, and Zico Kolter, editors, AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25 - March 4, 2025, Philadelphia, PA, USA, pages 11122-11130. AAAI Press, 2025. URL: https://doi.org/10.1609/AAAI.V39I11.33209.
  10. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified dominance and symmetry breaking for combinatorial optimisation. J. Artif. Intell. Res., 77:1539-1589, 2023. URL: https://doi.org/10.1613/jair.1.14296.
  11. Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. A modular approach to MaxSAT modulo theories. In Matti Järvisalo and Allen Van Gelder, editors, Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, volume 7962 of Lecture Notes in Computer Science, pages 150-165. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_12.
  12. Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Jimmy Ho-Man Lee, editor, Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings, volume 6876 of Lecture Notes in Computer Science, pages 225-239. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23786-7_19.
  13. Jessica Davies and Fahiem Bacchus. Exploiting the power of mip solvers in MaxSAT. In Matti Järvisalo and Allen Van Gelder, editors, Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, volume 7962 of Lecture Notes in Computer Science, pages 166-181. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_13.
  14. Jessica Davies and Fahiem Bacchus. Postponing optimization to speed up MAXSAT solving. In Christian Schulte, editor, Principles and Practice of Constraint Programming - 19th International Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, volume 8124 of Lecture Notes in Computer Science, pages 247-262. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40627-0_21.
  15. Toby O. Davies, Graeme Gange, and Peter J. Stuckey. Automatic logic-based benders decomposition with minizinc. In Satinder Singh and Shaul Markovitch, editors, Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, February 4-9, 2017, San Francisco, California, USA, pages 787-793. AAAI Press, 2017. URL: https://doi.org/10.1609/AAAI.V31I1.10654.
  16. Erin Delisle and Fahiem Bacchus. Solving weighted CSPs by successive relaxations. In Christian Schulte, editor, Principles and Practice of Constraint Programming - 19th International Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, volume 8124 of Lecture Notes in Computer Science, pages 273-281. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40627-0_23.
  17. Jo Devriendt, Bart Bogaerts, and Maurice Bruynooghe. BreakIDGlucose: On the importance of row symmetry in SAT. In CSPSAT, Vienna, 18 July 2014, pages 1-17, July 2014. URL: https://lirias.kuleuven.be/handle/123456789/456639.
  18. Jo Devriendt, Bart Bogaerts, and Maurice Bruynooghe. Symmetric explanation learning: Effective dynamic symmetry handling for SAT. 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 83-100. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_6.
  19. Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe, and Marc Denecker. Improved static symmetry breaking for SAT. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 104-122. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_8.
  20. 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. URL: https://doi.org/10.24963/ijcai.2018/180.
  21. Katalin Fazekas, Fahiem Bacchus, and Armin Biere. Implicit hitting set algorithms for maximum satisfiability modulo theories. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of Lecture Notes in Computer Science, pages 134-151. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_10.
  22. Ana Graça, Inês Lynce, João Marques-Silva, and Arlindo L. Oliveira. Efficient and accurate haplotype inference by combining parsimony and pedigree information. In Katsuhisa Horimoto, Masahiko Nakatsui, and Nikolaj Popov, editors, Algebraic and Numeric Biology - 4th International Conference, ANB 2010, Hagenberg, Austria, July 31- August 2, 2010, Revised Selected Papers, volume 6479 of Lecture Notes in Computer Science, pages 38-56. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-28067-2_3.
  23. Alexey Ignatiev, Mikolás Janota, and João Marques-Silva. Quantified maximum satisfiability. Constraints An Int. J., 21(2):277-302, 2016. URL: https://doi.org/10.1007/S10601-015-9195-9.
  24. Markus Kirchweger and Stefan Szeider. SAT modulo symmetries for graph generation and enumeration. ACM Trans. Comput. Log., 25(3):1-30, 2024. URL: https://doi.org/10.1145/3670405.
  25. Javier Larrosa, Conrado Martínez, and Emma Rollon. Theoretical and empirical analysis of cost-function merging for implicit hitting set WCSP solving. In Michael J. Wooldridge, Jennifer G. Dy, and Sriraam Natarajan, editors, Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada, pages 8057-8064. AAAI Press, 2024. URL: https://doi.org/10.1609/AAAI.V38I8.28644.
  26. Hakan Metin, Souheib Baarir, Maximilien Colange, and Fabrice Kordon. CDCLSym: Introducing effective symmetry breaking in SAT solving. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I, volume 10805 of Lecture Notes in Computer Science, pages 99-114. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89960-2_6.
  27. Erick Moreno-Centeno and Richard M. Karp. The implicit hitting set approach to solve combinatorial optimization problems with an application to multigenome alignment. Oper. Res., 61(2):453-468, 2013. URL: https://doi.org/10.1287/OPRE.1120.1139.
  28. Andreas Niskanen, Jere Mustonen, Jeremias Berg, and Matti Järvisalo. Computing smallest MUSes of quantified Boolean formulas. In Georg Gottlob, Daniela Inclezan, and Marco Maratea, editors, Logic Programming and Nonmonotonic Reasoning - 16th International Conference, LPNMR 2022, Genova, Italy, September 5-9, 2022, Proceedings, volume 13416 of Lecture Notes in Computer Science, pages 301-314. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15707-3_23.
  29. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log., 62(3):981-998, 1997. URL: https://doi.org/10.2307/2275583.
  30. James A. Reggia, Dana S. Nau, and Pearl Y. Wang. Diagnostic expert systems based on a set covering model. Int. J. Man Mach. Stud., 19(5):437-460, 1983. URL: https://doi.org/10.1016/S0020-7373(83)80065-0.
  31. Raymond Reiter. A theory of diagnosis from first principles. Artif. Intell., 32(1):57-95, 1987. URL: https://doi.org/10.1016/0004-3702(87)90062-2.
  32. Ashish Sabharwal. Symchaff: exploiting symmetry in a structure-aware satisfiability solver. Constraints An Int. J., 14(4):478-505, 2009. URL: https://doi.org/10.1007/s10601-008-9060-1.
  33. Paul Saikko, Jeremias Berg, and Matti Järvisalo. LMHS: A SAT-IP hybrid MaxSAT solver. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 539-546. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_34.
  34. Paul Saikko, Carmine Dodaro, Mario Alviano, and Matti Järvisalo. A hybrid approach to optimization in answer set programming. In Michael Thielscher, Francesca Toni, and Frank Wolter, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018, Tempe, Arizona, 30 October - 2 November 2018, pages 32-41. AAAI Press, 2018. URL: https://aaai.org/ocs/index.php/KR/KR18/paper/view/18021.
  35. Paul Saikko, Johannes Peter Wallner, and Matti Järvisalo. Implicit hitting set algorithms for reasoning beyond NP. In Chitta Baral, James P. Delgrande, and Frank Wolter, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, Cape Town, South Africa, April 25-29, 2016, pages 104-113. AAAI Press, 2016. URL: http://www.aaai.org/ocs/index.php/KR/KR16/paper/view/12812.
  36. Pavel Smirnov. Pseudo-boolean optimization by implicit hitting sets. Master’s thesis, University of Helsinki, 2021. URL: http://hdl.handle.net/10138/340857.
  37. Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. Pseudo-Boolean optimization by implicit hitting sets. 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 51:1-51:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.51.
  38. 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.
  39. Rodrigue Konan Tchinda and Clémentin Tayou Djamégni. On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers. Constraints An Int. J., 25(3-4):251-279, 2020. URL: https://doi.org/10.1007/s10601-020-09313-2.
  40. Daimy Van Caudenberg and Bart Bogaerts. Symmetry and dominance breaking for pseudo-Boolean optimization. In Toon Calders, Celine Vens, Jefrey Lijffijt, and Bart Goethals, editors, Artificial Intelligence and Machine Learning - 34th Joint Benelux Conference, BNAIC/Benelearn 2022, Mechelen, Belgium, November 7-9, 2022, Revised Selected Papers, volume 1805 of Communications in Computer and Information Science, pages 149-166. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-39144-6_10.
  41. Daimy Van Caudenberg, Bart Bogaerts, and Leandro Vendramin. Incremental SAT-based enumeration of solutions to the yang-baxter equation. In Arie Gurfinkel and Marijn Heule, editors, Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part II, volume 15697 of Lecture Notes in Computer Science, pages 3-22. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90653-4_1.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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