Document Open Access Logo

HitPBO: An Implicit Hitting Set Solver for Pseudo-Boolean Optimization (Tool Paper)

Authors Hannes Ihalainen , Dieter Vandesande , André Schidler , Jeremias Berg , Matti Järvisalo

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.34.pdf
  • Filesize: 1.08 MB
  • 13 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorial optimization
  • Theory of computation → Constraint and logic programming
Keywords
  • Pseudo-Boolean optimization
  • implicit hitting set approach
  • solvers

Metrics

Abstract

We describe HitPBO 1.0, a from-scratch open-source C++ implementation of the implicit hitting set (IHS) approach to pseudo-Boolean optimization. Compared to earlier implementations, HitPBO adds a range of functionalities and search techniques, certificates, and support for various alternative solvers within IHS. We give an overview of the solver’s architecture and its functionalities.

Cite As Get BibTex

Hannes Ihalainen, Dieter Vandesande, André Schidler, Jeremias Berg, and Matti Järvisalo. HitPBO: An Implicit Hitting Set Solver for Pseudo-Boolean Optimization (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.34

Author Details

Hannes Ihalainen
  • Department of Computer Science, University of Helsinki, Finland
Dieter Vandesande
  • Department of Computer Science, Vrije Universiteit Brussel, Belgium
  • Department of Computer Science, KU Leuven, Belgium
André Schidler
  • Chair of Computer Architecture, University of Freiburg, Germany
Jeremias Berg
  • Department of Computer Science, University of Helsinki, Finland
Matti Järvisalo
  • Department of Computer Science, University of Helsinki, Finland

Funding

  • Ihalainen, Hannes: Funded by University of Helsinki Doctoral Program in Computer Science and Research Council of Finland grant 356046.
  • Vandesande, Dieter: Funded by the Fonds Wetenschappelijk Onderzoek – Vlaanderen fellowship 11A5J25N.
  • Schidler, André: Funded by German Research Foundation (DFG) through grant INST 35/1597-1 FUGG.
  • Berg, Jeremias: Funded by Research Council of Finland grant 362987.
  • Järvisalo, Matti: Funded by Research Council of Finland grant 356046.

Acknowledgements

The authors wish to thank the Finnish Computing Competence Infrastructure (FCCI) and the state of Baden-Württemberg through bwHPC for supporting this project with computational and data storage resources.

Supplementary Materials

References

  1. Tobias Achterberg. SCIP: Solving constraint integer programs. Math. Program. Comput., 1(1):1-41, 2009. URL: https://doi.org/10.1007/S12532-008-0001-1.
  2. Tobias Achterberg, Robert E. Bixby, Zonghao Gu, Edward Rothberg, and Dieter Weninger. Presolve reductions in mixed integer programming. INFORMS J. Comput., 32(2):473-506, 2020. URL: https://doi.org/10.1287/IJOC.2018.0857.
  3. Carlos Ansótegui, Maria Luisa Bonet, Joel Gabàs, and Jordi Levy. Improving SAT-based weighted MaxSAT solvers. In Michela Milano, editor, Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings, Lecture Notes in Computer Science, pages 86-101. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_9.
  4. Gilles Audemard, Jean-Marie Lagniez, and Laurent Simon. Improving glucose for incremental SAT solving with assumptions: Application to MUS extraction. 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 309-317. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_23.
  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. 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, Lecture Notes in Computer Science, pages 652-670. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_42.
  7. Daniel Le Berre and Anne Parrain. The sat4j library, release 2.2. J. Satisf. Boolean Model. Comput., 7(2-3):59-6, 2010. URL: https://doi.org/10.3233/SAT190075.
  8. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  9. 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.
  10. Der-San Chen, Robert G. Batson, and Yu Dang. Applied Integer Programming: Modeling and Solution. John Wiley & Sons, 2009. Google Scholar
  11. Vasek Chvátal. Edmonds polytopes and a hierarchy of combinatorial problems. Discret. Math., 4(4):305-337, 1973. URL: https://doi.org/10.1016/0012-365X(73)90167-2.
  12. IIBM ILOG Cplex et al. V12. 1: User’s manual for cplex. International business machines corporation, 46(53):157, 2009. Google Scholar
  13. Harlan P. Crowder, Ellis L. Johnson, and Manfred W. Padberg. Solving large-scale zero-one linear programming problems. Oper. Res., 31(5):803-834, 1983. URL: https://doi.org/10.1287/OPRE.31.5.803.
  14. George Bernard Dantzig, Delbert R Fulkerson, and Selmer Martin Johnson. On a linear-programming, combinatorial approach to the traveling-salesman problem. Operations Research, 7(1):58-66, 1959. URL: https://doi.org/10.1287/opre.7.1.58.
  15. 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, Lecture Notes in Computer Science, pages 247-262. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40627-0_21.
  16. 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.
  17. 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://doi.org/10.1609/AAAI.V35I5.16492.
  18. Leon Eifler and Ambros M. Gleixner. A computational status update for exact rational mixed integer programming. Math. Program., 197(2):793-812, 2023. URL: https://doi.org/10.1007/S10107-021-01749-5.
  19. 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.
  20. Exact. URL: https://gitlab.com/nonfiction-software/exact.
  21. Ambros M. Gleixner, Leona Gottwald, and Alexander Hoen. PaPILO: A parallel presolving library for integer and linear optimization with multiprecision support. INFORMS Journal on Computing, 35(6):1329-1341, 2023. URL: https://doi.org/10.1287/IJOC.2022.0171.
  22. Stephan Gocht and Jakob Nordström. Certifying parity reasoning efficiently using pseudo-boolean proofs. 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 3768-3777. AAAI Press, 2021. URL: https://doi.org/10.1609/AAAI.V35I5.16494.
  23. Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2026. URL: https://www.gurobi.com.
  24. Christopher Hojny, Mathieu Besançon, Ksenia Bestuzheva, Sander Borst, Joao Dionísio, Johannes Ehls, Leon Eifler, Mohammed Ghannam, Ambros Gleixner, Adrian Göß, Alexander Hoen, Jacob von Holly-Ponientzietz, Rolf van der Hulst, Dominik Kamp, Thorsten Koch, Kevin Kofler, Jurgen Lentz, Marco Lübbecke, Stephen J. Maher, Paul Matti Meinhold, Gioni Mexi, Til Mohr, Erik Mühmer, Krunal Kishor Patel, Marc E. Pfetsch, Sebastian Pokutta, Chantal Reinartz Groba, Felipe Serrano, Yuji Shinano, Mark Turner, Stefan Vigerske, Matthias Walter, Dieter Weninger, and Liding Xu. The SCIP Optimization Suite 10.0, 2025. URL: https://arxiv.org/abs/2511.18580.
  25. Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts. Symmetric core learning for pseudo-boolean optimization by implicit hitting sets. In Maria Garcia de la Banda, editor, 31st International Conference on Principles and Practice of Constraint Programming, CP 2025, Glasgow, Scotland, August 10-15, 2025, volume 340 of LIPIcs, pages 15:1-15:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CP.2025.15.
  26. Hannes Ihalainen, Dieter Vandesande, André Schidler, Jeremias Berg, Bart Bogaerts, and Matti Järvisalo. Efficient and reliable hitting-set computations for the implicit hitting set approach. In Sven Koenig, Chad Jenkins, and Matthew E. Taylor, editors, Fortieth AAAI Conference on Artificial Intelligence, Thirty-Eighth Conference on Innovative Applications of Artificial Intelligence, Sixteenth Symposium on Educational Advances in Artificial Intelligence, AAAI 2026, Singapore, January 20-27, 2026, pages 14251-14260. AAAI Press, 2026. URL: https://doi.org/10.1609/AAAI.V40I17.38439.
  27. João Marques-Silva, Josep Argelich, Ana Graça, and Inês Lynce. Boolean lexicographic optimization: Algorithms & applications. Ann. Math. Artif. Intell., 62(3-4):317-343, 2011. URL: https://doi.org/10.1007/S10472-011-9233-2.
  28. Pseudo-Boolean Competition 2025. URL: https://www.cril.univ-artois.fr/PB25/.
  29. PBO-IHS. Pseudo-Boolean optimization (PBO) solver that utilizes the implicit hitting set (IHS) approach. URL: https://bitbucket.org/coreo-group/pbo-ihs-solver/.
  30. PBComp24-cg Mixed-Bag & PB-OLL-RS. URL: https://bitbucket.org/coreo-group/pbcomp24-cg.
  31. RoundingSat. The pseudo-Boolean solver powered by proof complexity! URL: https://gitlab.com/MIAOresearch/software/roundingsat.
  32. Paul Saikko. Implicit Hitting Set Algorithms for Constraint Optimization. PhD thesis, University of Helsinki, Finland, 2019. Google Scholar
  33. Masahiko Sakai and Hidetomo Nabeshima. Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers. IEICE Trans. Inf. Syst., 98-D(6):1121-1127, 2015. URL: https://doi.org/10.1587/TRANSINF.2014FOP0007.
  34. 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.
  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. VeriPB Prooflogger, a library for proof logging in the VeriPB proof format. URL: https://github.com/DietVds/VeriPB_Prooflogger.
  37. Dag Wedelin. An algorithm for large scale 0-1 integer programming with application to airline crew scheduling. Annals of Operations Research, 57(1):283-301, 1995. URL: https://doi.org/10.1007/BF02099703.
  38. Yujiao Zhao, Yiyuan Wang, Yi Chu, Wenbo Zhou, Shaowei Cai, and Minghao Yin. Improving local search algorithm for pseudo boolean optimization. J. Artif. Intell. Res., 83, 2025. URL: https://doi.org/10.1613/JAIR.1.16626.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact