Document Open Access Logo

PACE Solver Description: Minimum Hitting Set Computation via Core-Guided MaxSAT Solving

Author André Schidler

PDF

File

Thumbnail PDF
PDF
LIPIcs.IPEC.2025.37.pdf
  • Filesize: 0.49 MB
  • 4 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Discrete optimization
  • Theory of computation → Constraint and logic programming
  • Theory of computation → Automated reasoning
Keywords
  • hitting set
  • maxsat
  • core-guided

Metrics

Abstract

This paper describes our hybrid MaxSAT and mixed integer programming approach for finding minimum hitting sets as submitted to the 2025 PACE challenge. We also discuss hitting set specific challenges, lower bounds, preprocessing and design choices.

Cite As Get BibTex

André Schidler. PACE Solver Description: Minimum Hitting Set Computation via Core-Guided MaxSAT Solving. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 37:1-37:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.IPEC.2025.37

Author Details

André Schidler
  • University of Freiburg, Germany

Funding

Funded by an Amazon Research Award (Fall/2023).

Supplementary Materials

References

  1. Benjamin Andres, Benjamin Kaufmann, Oliver Matheis, and Torsten Schaub. Unsatisfiability-based optimization in clasp. In ICLP (Technical Communications), volume 17 of LIPIcs, pages 211-221. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPICS.ICLP.2012.211.
  2. Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, and Dieter Vandesande. Certified core-guided maxsat solving. In Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings, volume 14132 of Lecture Notes in Computer Science, pages 1-22. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-38499-8_1.
  3. Jeremias Berg, Matti Järvisalo, Ruben Martins, Andreas Niskanen, and Tobias Paxian. MaxSAT Evaluation 2024: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2024. Google Scholar
  4. Ksenia Bestuzheva, Mathieu Besançon, Wei-Kun Chen, Antonia Chmiela, Tim Donkiewicz, Jasper van Doornmalen, Leon Eifler, Oliver Gaul, Gerald Gamrath, Ambros Gleixner, Leona Gottwald, Christoph Graczyk, Katrin Halbig, Alexander Hoen, Christopher Hojny, Rolf van der Hulst, Thorsten Koch, Marco Lübbecke, Stephen J. Maher, Frederic Matter, Erik Mühmer, Benjamin Müller, Marc E. Pfetsch, Daniel Rehfeldt, Steffan Schlein, Franziska Schlösser, Felipe Serrano, Yuji Shinano, Boro Sofranac, Mark Turner, Stefan Vigerske, Fabian Wegscheider, Philipp Wellner, Dieter Weninger, and Jakob Witzig. The SCIP Optimization Suite 8.0. ZIB-Report 21-41, Zuse Institute Berlin, December 2021. Google Scholar
  5. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In CAV, 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.
  6. Thomas Bläsius, Tobias Friedrich, David Stangl, and Christopher Weyand. An efficient branch-and-bound solver for hitting set. In Proceedings of the Symposium on Algorithm Engineering and Experiments, ALENEX 2022, Alexandria, VA, USA, January 9-10, 2022, pages 209-220. SIAM, 2022. URL: https://doi.org/10.1137/1.9781611977042.17.
  7. Yi Chu, Shaowei Cai, and Chuan Luo. Nuwls: Improving local search for (weighted) partial maxsat by new weighting techniques. In 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://doi.org/10.1609/AAAI.V37I4.25505.
  8. William J. Cook, Thorsten Koch, Daniel E. Steffy, and Kati Wolter. A hybrid branch-and-bound approach for exact rational mixed-integer programming. Math. Program. Comput., 5(3):305-344, 2013. URL: https://doi.org/10.1007/S12532-013-0055-6.
  9. Jessica Davies and Fahiem Bacchus. Exploiting the power of MIP solvers in MaxSat. In SAT, 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.
  10. Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  11. Alexey Ignatiev, António Morgado, and João Marques-Silva. RC2: an efficient maxsat solver. J. Satisf. Boolean Model. Comput., 11(1):53-64, 2019. URL: https://doi.org/10.3233/SAT190116.
  12. Richard M. Karp. Reducibility among combinatorial problems. In Proceedings of a symposium on the Complexity of Computer Computations, held March 20-22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York, USA, The IBM Research Symposia Series, pages 85-103. Plenum Press, New York, 1972. URL: https://doi.org/10.1007/978-1-4684-2001-2_9.
  13. Rafael Kiesel and André Schidler. PACE solver description: Dager - cutting out cycles with maxsat. In 17th International Symposium on Parameterized and Exact Computation, IPEC 2022, September 7-9, 2022, Potsdam, Germany, volume 249 of LIPIcs, pages 32:1-32:4. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.IPEC.2022.32.
  14. Rafael Kiesel and André Schidler. A dynamic maxsat-based approach to directed feedback vertex sets. In Proceedings of the Symposium on Algorithm Engineering and Experiments, ALENEX 2023, Florence, Italy, January 22-23, 2023, pages 39-52. SIAM, 2023. URL: https://doi.org/10.1137/1.9781611977561.CH4.
  15. António Morgado, Carmine Dodaro, and João Marques-Silva. Core-guided MaxSAT with soft cardinality constraints. In CP, volume 8656 of Lecture Notes in Computer Science, pages 564-573. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10428-7_41.
  16. Paul Saikko, Jeremias Berg, and Matti Järvisalo. LMHS: A SAT-IP hybrid MaxSAT solver. In SAT, 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.
  17. André Schidler and Stefan Szeider. Analyzing reformulation performance in core-guided maxsat solving. In 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, August 12-15, 2025, Glasgow, Scotland, volume 341 of LIPIcs, pages 26:1-26:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.26.
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