Document Open Access Logo

Scuttle: A System for Multi-Objective MaxSAT (Tool Paper)

Authors Christoph Jabs , Jeremias Berg , Matti Järvisalo

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.37.pdf
  • Filesize: 1.22 MB
  • 13 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorial optimization
  • Theory of computation → Constraint and logic programming
Keywords
  • Multi-objective combinatorial optimization
  • maximum satisfiability
  • pseudo-Boolean optimization

Metrics

Abstract

We describe the Scuttle system for multi-objective combinatorial optimization. Scuttle accepts multi-objective instances where the constraints are declared either as propositional clauses or pseudo-Boolean constraints, and implements a range of multi-objective maximum satisfiability algorithms (including ones for enumerating all Pareto-optimal and leximax-optimal solutions). Pseudo-Boolean constraints are translated to clauses, allowing for applying any of the implemented algorithms on both the clausal and the pseudo-Boolean level. Scuttle also includes tightly integrated preprocessing (both core boosting and liftings of SAT preprocessing techniques) for multi-objective instances and can provide proof certificates for selected algorithms.

Cite As Get BibTex

Christoph Jabs, Jeremias Berg, and Matti Järvisalo. Scuttle: A System for Multi-Objective MaxSAT (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 37:1-37:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.37

Author Details

Christoph Jabs
  • Department of Computer Science, University of Helsinki, Finland
Jeremias Berg
  • Department of Computer Science, University of Helsinki, Finland
Matti Järvisalo
  • Department of Computer Science, University of Helsinki, Finland

Funding

  • Jabs, Christoph: Funded by Research Council of Finland grant 356046.
  • 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) for supporting this project with computational and data storage resources.

Supplementary Materials

References

  1. Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo, and Yong Kiam Tan. Faster certified symmetry breaking using orders with auxiliary variables. 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 14140-14148. AAAI Press, 2026. URL: https://doi.org/10.1609/aaai.v40i17.38426.
  2. 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, volume 7514 of Lecture Notes in Computer Science, pages 86-101. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_9.
  3. Fahiem Bacchus, Antti Hyttinen, Matti Järvisalo, and Paul Saikko. Reduced cost fixing for maximum satisfiability. 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 5209-5213. ijcai.org, 2018. URL: https://doi.org/10.24963/ijcai.2018/723.
  4. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiability. 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 929-991. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201008.
  5. Olivier Bailleux and Yacine Boufkhad. Efficient CNF encoding of Boolean cardinality constraints. In Francesca Rossi, editor, Principles and Practice of Constraint Programming - CP 2003, 9th International Conference, CP 2003, Kinsale, Ireland, September 29 - October 3, 2003, Proceedings, volume 2833 of Lecture Notes in Computer Science, pages 108-122. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45193-8_8.
  6. Jeremias Berg, Matti Järvisalo, Ruben Martins, Andreas Niskanen, and Tobias Paxian. MaxSAT Evaluation 2024: Rules. URL: https://maxsat-evaluations.github.io/2024/rules.html.
  7. Jeremias Berg, Paul Saikko, and Matti Järvisalo. Subsumed label elimination for maximum satisfiability. In Gal A. Kaminka, Maria Fox, Paolo Bouquet, Eyke Hüllermeier, Virginia Dignum, Frank Dignum, and Frank van Harmelen, editors, ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016), volume 285 of Frontiers in Artificial Intelligence and Applications, pages 630-638. IOS Press, 2016. URL: https://doi.org/10.3233/978-1-61499-672-9-630.
  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. Journal of Artificial Intelligence Research, 77:1539-1589, 2023. URL: https://doi.org/10.1613/jair.1.14296.
  10. Miguel Cabral, Mikolás Janota, and Vasco Manquinho. SAT-based leximax optimisation algorithms. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, Haifa, Israel, August 2-5, 2022, volume 236 of LIPIcs, pages 29:1-29:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.29.
  11. João Cortes, Inês Lynce, and Vasco Manquinho. New core-guided and hitting set algorithms for multi-objective combinatorial optimization. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, volume 13994 of Lecture Notes in Computer Science, pages 55-73. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_7.
  12. 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.
  13. Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Fahiem Bacchus and Toby Walsh, editors, Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings, volume 3569 of Lecture Notes in Computer Science, pages 61-75. Springer, 2005. URL: https://doi.org/10.1007/11499107_5.
  14. Matthias Ehrgott. Multicriteria Optimization (2. ed.). Springer, 2005. URL: https://doi.org/10.1007/3-540-27659-9.
  15. Jon William Freeman. Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, University of Pennsylvania, USA, 1995. Google Scholar
  16. James F. Gimpel. A reduction technique for prime implicant tables. In 5th Annual Symposium on Switching Circuit Theory and Logical Design, Princeton, New Jersey, USA, November 11-13, 1964, pages 183-191. IEEE Computer Society, 1964. URL: https://doi.org/10.1109/SWCT.1964.4.
  17. 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.
  18. Andreia P. Guerreiro, João Cortes, Daniel Vanderpooten, Cristina Bazgan, Inês Lynce, Vasco Manquinho, and José Rui Figueira. Exact and approximate determination of the Pareto front using minimal correction subsets. Computers & Operations Research, 153:106153, 2023. URL: https://doi.org/10.1016/j.cor.2023.106153.
  19. Qi Huangfu and J. A. J. Hall. Parallelizing the dual revised simplex method. Mathematical Programming Computation, 10:119-142, 2018. URL: https://doi.org/10.1007/s12532-017-0130-5.
  20. Alexey Ignatiev, António Morgado, and João Marques-Silva. RC2: an efficient MaxSAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 11:53-64, 2019. URL: https://doi.org/10.3233/SAT190116.
  21. Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Clause redundancy and preprocessing in maximum satisfiability. In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 75-94. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_6.
  22. 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.
  23. Christoph Jabs. RustSAT: A library for SAT solving in rust. In Jeremias Berg and Jakob Nordström, editors, 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Glasgow, Scotland, August 12-15, 2025, volume 341 of LIPIcs, pages 15:1-15:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.15.
  24. Christoph Jabs, Jeremias Berg, Bart Bogaerts, and Matti Järvisalo. Certifying pareto optimality in multi-objective maximum satisfiability. 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 108-129. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90653-4_6.
  25. Christoph Jabs, Jeremias Berg, Hannes Ihalainen, and Matti Järvisalo. Preprocessing in SAT-based multi-objective combinatorial optimization. In Roland H. C. Yap, editor, 29th International Conference on Principles and Practice of Constraint Programming, CP 2023, Toronto, Canada, August 27-31, 2023, volume 280 of LIPIcs, pages 18:1-18:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CP.2023.18.
  26. Christoph Jabs, Jeremias Berg, and Matti Järvisalo. Core boosting in SAT-based multi-objective optimization. In Bistra Dilkina, editor, Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 21st International Conference, CPAIOR 2024, Uppsala, Sweden, May 28-31, 2024, Proceedings, Part II, volume 14743 of Lecture Notes in Computer Science, pages 1-19. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-60599-4_1.
  27. Christoph Jabs, Jeremias Berg, and Matti Järvisalo. Engineering and evaluating multi-objective pseudo-Boolean optimizers. In Giovanni Casini, Besik Dundua, and Temur Kutsia, editors, Logics in Artificial Intelligence - 19th European Conference, JELIA 2025, Kutaisi, Georgia, September 1-4, 2025, Proceedings, Part I, volume 16093 of Lecture Notes in Computer Science, pages 115-134. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-04587-4_8.
  28. Christoph Jabs, Jeremias Berg, and Matti Järvisalo. Multi-objective maximum satisfiability by single-objective implicit hitting set optimization. In Tias Guns, editor, Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 23rd International Conference, CPAIOR 2026, Rabat, Morocco, May 26-29, 2026, volume 16595 of Lecture Notes in Computer Science. Springer, 2026. URL: https://media.christophjabs.info/papers/JabsEtAl2026MultiObjectiveMaximumSatisfiability.pdf.
  29. Christoph Jabs, Jeremias Berg, Andreas Niskanen, and Matti Järvisalo. From single-objective to bi-objective maximum satisfiability solving. Journal of Artificial Intelligence Research, 80:1223-1269, 2024. URL: https://doi.org/10.1613/jair.1.15333.
  30. Daniel Jackson, H.-Christian Estler, and Derek Rayside. The guided improvement algorithm for exact, general-purpose, many-objective combinatorial optimization. Technical report, Compute Science and Artificial Intelligence Laboratory, 2009. URL: http://hdl.handle.net/1721.1/46322.
  31. Matti Järvisalo, Armin Biere, and Marijn Heule. Blocked clause elimination. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 129-144. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_10.
  32. Saurabh Joshi, Ruben Martins, and Vasco Manquinho. Generalized totalizer encoding for pseudo-Boolean constraints. In Gilles Pesant, editor, Principles and Practice of Constraint Programming - 21st International Conference, CP 2015, Cork, Ireland, August 31 - September 4, 2015, Proceedings, volume 9255 of Lecture Notes in Computer Science, pages 200-209. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23219-5_15.
  33. Tuukka Korhonen, Jeremias Berg, Paul Saikko, and Matti Järvisalo. MaxPre: An extended MaxSAT preprocessor. 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 449-456. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_28.
  34. Miyuki Koshimura, Hidetomo Nabeshima, Hiroshi Fujita, and Ryuzo Hasegawa. Minimal model generation with respect to an atom set. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Proceedings of the 7th International Workshop on First-Order Theorem Proving, FTP 2009, Oslo, Norway, July 6-7, 2009, volume 556 of CEUR Workshop Proceedings. CEUR-WS.org, 2009. URL: https://ceur-ws.org/Vol-556/paper06.pdf.
  35. Daniel Le Berre. Exploiting the real power of unit propagation lookahead. Electronic Notes in Discrete Mathematics, 9:59-80, 2001. URL: https://doi.org/10.1016/S1571-0653(04)00314-2.
  36. João Marques-Silva and Jordi Planes. On using unsatisfiability for solving maximum satisfiability. Computing Research Repository, abs/0712.1097, 2007. URL: https://arxiv.org/abs/0712.1097.
  37. Ruben Martins, Saurabh Joshi, Vasco Manquinho, and Inês Lynce. Incremental cardinality constraints for MaxSAT. In Barry O'Sullivan, editor, Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Lyon, France, September 8-12, 2014. Proceedings, volume 8656 of Lecture Notes in Computer Science, pages 531-548. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10428-7_39.
  38. António Morgado, Carmine Dodaro, and João Marques-Silva. Core-guided MaxSAT with soft cardinality constraints. In Barry O'Sullivan, editor, Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Lyon, France, September 8-12, 2014. Proceedings, 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.
  39. Richard Ostrowski, Éric Grégoire, Bertrand Mazure, and Lakhdar Sais. Recovering and exploiting structural knowledge from CNF formulas. In Pascal Van Hentenryck, editor, Principles and Practice of Constraint Programming - CP 2002, 8th International Conference, CP 2002, Ithaca, NY, USA, September 9-13, 2002, Proceedings, volume 2470 of Lecture Notes in Computer Science, pages 185-199. Springer, 2002. URL: https://doi.org/10.1007/3-540-46135-3_13.
  40. Tobias Paxian, Pascal Raiola, and Bernd Becker. On preprocessing for weighted MaxSAT. In Fritz Henglein, Sharon Shoham, and Yakir Vizel, editors, Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings, volume 12597 of Lecture Notes in Computer Science, pages 556-577. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-67067-2_25.
  41. Olivier Roussel. General OPB format. URL: https://www.cril.univ-artois.fr/PB24/OPBgeneral.pdf.
  42. Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, and Daniel Le Berre. Solving multiobjective discrete optimization problems with propositional minimal model generation. 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 596-614. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_38.
  43. John Sylva and Alejandro Crema. A method for finding the set of non-dominated vectors for multiple objective integer linear programs. European Journal of Operational Research, 158:46-55, 2004. URL: https://doi.org/10.1016/S0377-2217(03)00255-8.
  44. Miguel Terra-Neves, Inês Lynce, and Vasco Manquinho. Multi-objective optimization through Pareto minimal correction subsets. 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 5379-5383. ijcai.org, 2018. URL: https://doi.org/10.24963/ijcai.2018/757.
  45. Ramin Zabih and David A. McAllester. A rearrangement search strategy for determining propositional satisfiability. In Howard E. Shrobe, Tom M. Mitchell, and Reid G. Smith, editors, Proceedings of the 7th National Conference on Artificial Intelligence, St. Paul, MN, USA, August 21-26, 1988, pages 155-160. AAAI Press / The MIT Press, 1988. URL: http://www.aaai.org/Library/AAAI/1988/aaai88-028.php.
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