Core Boosting in SAT-Based Multi-objective Optimization | SpringerLink
Skip to main content
Springer Nature Link
Log in

Core Boosting in SAT-Based Multi-objective Optimization

  • Conference paper
  • First Online:
Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14743))

  • 343 Accesses

Abstract

Maximum satisfiability (MaxSAT) constitutes today a successful approach to solving various real-world optimization problems through propositional encodings. Building on this success, approaches have recently been proposed for finding Pareto-optimal solutions to multi-objective MaxSAT (MO-MaxSAT) instances, i.e., propositional encodings under multiple objective functions. In this work, we propose core boosting as a reformulation/preprocessing technique for improving the runtime performance of MO-MaxSAT solvers. Core boosting in the multi-objective setting allows for shrinking the ranges of the multiple objectives at hand, which can be particularly beneficial for MO-MaxSAT relying on search that requires enforcing increasingly tighter objective bounds through propositional encodings. We show that core boosting is effective in improving the runtime performance of SAT-based MO-MaxSAT solvers typically with little overhead.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 14871
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 9437
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    In practice, the algorithms considered in this work often employ an implication relationship—\(\tau (\langle O \le B \rangle ) = 1\) if \(\tau \) satisfies \(O\le B\)—rather than the mentioned equivalence. We assume equivalences for simplicity without loss of generality.

  2. 2.

    Exploring similar ideas from the perspective of so-called lower bound sets [20] constitutes interesting future work beyond the scope of this paper.

References

  1. Andres, B., Kaufmann, B., Matheis, O., Schaub, T.: Unsatisfiability-based optimization in clasp. In: Dovier, A., Costa, V.S. (eds.) Technical Communications of the 28th International Conference on Logic Programming, ICLP 2012, 4–8 September 2012, Budapest, Hungary. LIPIcs, vol. 17, pp. 211–221. Schloss Dagstuhl—Leibniz-Zentrum für Informatik (2012). https://doi.org/10.4230/LIPICS.ICLP.2012.211

  2. Ansótegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial MaxSAT through satisfiability testing. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 427–440. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_39

    Chapter  Google Scholar 

  3. Ansótegui, C., Didier, F., Gabàs, J.: Exploiting the structure of unsatisfiable cores in MaxSAT. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25–31 July 2015, pp. 283–289. AAAI Press (2015). http://ijcai.org/Abstract/15/046

  4. Ansótegui, C., Gabàs, J.: WPM3: an (in)complete algorithm for weighted partial MaxSAT. Artif. Intell. 250, 37–57 (2017). https://doi.org/10.1016/J.ARTINT.2017.05.003

    Article  MathSciNet  Google Scholar 

  5. Bacchus, F., Järvisalo, M., Martins, R.: Maximum satisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability—Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 929–991. IOS Press (2021). https://doi.org/10.3233/FAIA201008

  6. Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of Boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108–122. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45193-8_8

    Chapter  Google Scholar 

  7. Belov, A., Morgado, A., Marques-Silva, J.: SAT-based preprocessing for MaxSAT. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 96–111. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_7

    Chapter  Google Scholar 

  8. Berg, J., Demirović, E., Stuckey, P.J.: Core-boosted linear search for incomplete MaxSAT. In: Rousseau, L.-M., Stergiou, K. (eds.) CPAIOR 2019. LNCS, vol. 11494, pp. 39–56. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-19212-9_3

    Chapter  Google Scholar 

  9. Berg, J., Järvisalo, M.: Weight-aware core extraction in SAT-based MaxSAT solving. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 652–670. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66158-2_42

    Chapter  Google Scholar 

  10. Berg, J., Saikko, P., Järvisalo, M.: Subsumed label elimination for maximum satisfiability. In: Kaminka, G.A., et al. (eds.) 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). Frontiers in Artificial Intelligence and Applications, vol. 285, pp. 630–638. IOS Press (2016). https://doi.org/10.3233/978-1-61499-672-9-630

  11. Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. J. Satisf. Boolean Model. Comput. 7(2–3), 59–64 (2010). https://doi.org/10.3233/SAT190075

    Article  Google Scholar 

  12. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability—Second Edition. Frontiers in Artificial Intelligence and Applications, vol. 336. IOS Press (2021). https://doi.org/10.3233/FAIA336

  13. Biere, A., Järvisalo, M., Kiesl, B.: Preprocessing in SAT solving. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability—Second Edition. Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 391–435. IOS Press (2021). https://doi.org/10.3233/FAIA200992

  14. Cabral, M., Janota, M., Manquinho, V.M.: SAT-based leximax optimisation algorithms. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, 2–5 August 2022, Haifa, Israel. LIPIcs, vol. 236, pp. 29:1–29:19. Schloss Dagstuhl—Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPICS.SAT.2022.29

  15. Cortes, J., Lynce, I., Manquinho, V.M.: New core-guided and hitting set algorithms for multi-objective combinatorial optimization. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023, Part II. LNCS, vol. 13994, pp. 55–73. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-30820-8_7

    Chapter  Google Scholar 

  16. Devriendt, J., Gocht, S., Demirovic, E., Nordström, J., Stuckey, P.J.: 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, 2–9 February 2021, pp. 3750–3758. AAAI Press (2021). https://doi.org/10.1609/AAAI.V35I5.16492

  17. Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electron. Notes Theor. Comput. Sci. 89(4), 543–560 (2003). https://doi.org/10.1016/S1571-0661(05)82542-3

    Article  Google Scholar 

  18. Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. J. Satisf. Boolean Model. Comput. 2(1–4), 1–26 (2006). https://doi.org/10.3233/SAT190014

    Article  Google Scholar 

  19. Ehrgott, M.: Multicriteria Optimization, 2nd edn. Springer, Cham (2005). https://doi.org/10.1007/3-540-27659-9

    Book  Google Scholar 

  20. Ehrgott, M., Gandibleux, X.: Bound sets for biobjective combinatorial optimization problems. Comput. Oper. Res. 34(9), 2674–2694 (2007). https://doi.org/10.1016/J.COR.2005.10.003

    Article  MathSciNet  Google Scholar 

  21. Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_25

    Chapter  Google Scholar 

  22. Gange, G., Berg, J., Demirović, E., Stuckey, P.J.: Core-guided and core-boosted search for CP. In: Hebrard, E., Musliu, N. (eds.) CPAIOR 2020. LNCS, vol. 12296, pp. 205–221. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58942-4_14

    Chapter  Google Scholar 

  23. Guerreiro, A.P., et al.: Exact and approximate determination of the Pareto front using minimal correction subsets. Comput. Oper. Res. 153, 106153 (2023). https://doi.org/10.1016/J.COR.2023.106153

  24. Heras, F., Larrosa, J., de Givry, S., Schiex, T.: 2006 and 2007 Max-SAT Evaluations: Contributed instances. J. Satisf. Boolean Model. Comput. 4(2–4), 239–250 (2008). https://doi.org/10.3233/SAT190046

    Article  Google Scholar 

  25. Ignatiev, A., Morgado, A., Marques-Silva, J.: RC2: an efficient MaxSAT solver. J. Satisf. Boolean Model. Comput. 11(1), 53–64 (2019). https://doi.org/10.3233/SAT190116

    Article  MathSciNet  Google Scholar 

  26. Ihalainen, H., Berg, J., Järvisalo, M.: Refined core relaxation for core-guided MaxSAT solving. In: Michel, L.D. (ed.) 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), 25–29 October 2021. LIPIcs, vol. 210, pp. 28:1–28:19. Schloss Dagstuhl—Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPICS.CP.2021.28

  27. Jabs, C., Berg, J., Ihalainen, H., Järvisalo, M.: Preprocessing in SAT-based multi-objective combinatorial optimization. In: Yap, R.H.C. (ed.) 29th International Conference on Principles and Practice of Constraint Programming, CP 2023, 27–31 August 2023, Toronto, Canada. LIPIcs, vol. 280, pp. 18:1–18:20. Schloss Dagstuhl—Leibniz-Zentrum für Informatik (2023). https://doi.org/10.4230/LIPICS.CP.2023.18

  28. Jabs, C., Berg, J., Niskanen, A., Järvisalo, M.: MaxSAT-based bi-objective Boolean optimization. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, 2–5 August 2022, Haifa, Israel. LIPIcs, vol. 236, pp. 12:1–12:23. Schloss Dagstuhl—Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPICS.SAT.2022.12

  29. Janota, M., Lynce, I., Manquinho, V.M., Marques-Silva, J.: PackUp: tools for package upgradability solving. J. Satisf. Boolean Model. Comput. 8(1/2), 89–94 (2012). https://doi.org/10.3233/SAT190090

    Article  MathSciNet  Google Scholar 

  30. Joshi, S., Martins, R., Manquinho, V.: Generalized totalizer encoding for pseudo-Boolean constraints. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 200–209. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23219-5_15

    Chapter  Google Scholar 

  31. Koshimura, M., Nabeshima, H., Fujita, H., Hasegawa, R.: Minimal model generation with respect to an atom set. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proceedings of the 7th International Workshop on First-Order Theorem Proving, FTP 2009, Oslo, Norway, 6–7 July 2009. CEUR Workshop Proceedings, vol. 556. CEUR-WS.org (2009). https://ceur-ws.org/Vol-556/paper06.pdf

  32. Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: a partial Max-SAT solver. J. Satisf. Boolean Model. Comput. 8(1/2), 95–100 (2012). https://doi.org/10.3233/SAT190091

    Article  MathSciNet  Google Scholar 

  33. Maliotov, D., Meel, K.S.: MLIC: a MaxSAT-based framework for learning interpretable classification rules. In: Hooker, J. (ed.) CP 2018. LNCS, vol. 11008, pp. 312–327. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98334-9_21

    Chapter  Google Scholar 

  34. Marler, R., Arora, J.: Survey of multi-objective optimization methods for engineering. Struct. Multidisc. Optim. 26, 369–395 (2004). https://doi.org/10.1007/s00158-003-0368-6

    Article  MathSciNet  Google Scholar 

  35. Marques, R., Russo, L.M.S., Roma, N.: Flying tourist problem: flight time and cost minimization in complex routes. Expert Syst. Appl. 130, 172–187 (2019). https://doi.org/10.1016/J.ESWA.2019.04.024

    Article  Google Scholar 

  36. Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability—Second Edition. Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 133–182. IOS Press (2021). https://doi.org/10.3233/FAIA200987

  37. Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability. Computing Research Repository abs/0712.1097 (2007). http://arxiv.org/abs/0712.1097

  38. Martins, R.: ASP to MaxSAT: metro, ShiftDesign, TimeTabling and BioRepair. In: Ansotegui, C., Bacchus, F., Järvislo, M., Martins, R. (eds.) MaxSAT Evaluation 2017: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2017-2, p. 27. University of Helsinki (2017). http://hdl.handle.net/10138/228949

  39. Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531–548. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10428-7_39

    Chapter  Google Scholar 

  40. Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided MaxSAT with soft cardinality constraints. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 564–573. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10428-7_41

    Chapter  Google Scholar 

  41. Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: Brodley, C.E., Stone, P. (eds.) Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 27–31 July 2014, Québec City, Québec, Canada, pp. 2717–2723. AAAI Press (2014). https://doi.org/10.1609/AAAI.V28I1.9124

  42. Paxian, T., Raiola, P., Becker, B.: On preprocessing for weighted MaxSAT. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 556–577. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-67067-2_25

    Chapter  Google Scholar 

  43. Piotrów, M.: UWrMaxSat: Efficient solver for MaxSAT and pseudo-Boolean problems. In: 32nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2020, Baltimore, MD, USA, 9–11 November 2020, pp. 132–136. IEEE (2020). https://doi.org/10.1109/ICTAI50040.2020.00031

  44. Soh, T., Banbara, M., Tamura, N., Le Berre, D.: Solving multiobjective discrete optimization problems with propositional minimal model generation. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 596–614. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66158-2_38

    Chapter  Google Scholar 

  45. Terra-Neves, M., Lynce, I., Manquinho, V.M.: Multi-objective optimization through Pareto minimal correction subsets. In: Lang, J. (ed.) Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, 13–19 July 2018, Stockholm, Sweden, pp. 5379–5383. ijcai.org (2018). https://doi.org/10.24963/IJCAI.2018/757

  46. Paxian, T., Reimer, S., Becker, B.: Dynamic polynomial watchdog encoding for solving weighted MaxSAT. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 37–53. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_3

    Chapter  Google Scholar 

Download references

Acknowledgments

Work financially supported by Research Council of Finland (grants 342145, 356046). The authors thank the Finnish Computing Competence Infrastructure for computational and data storage resources.

Author information

Authors and Affiliations

  1. HIIT, Department of Computer Science, University of Helsinki, Helsinki, Finland

    Christoph Jabs, Jeremias Berg & Matti Järvisalo

Authors
  1. Christoph Jabs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jeremias Berg
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Matti Järvisalo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Christoph Jabs .

Editor information

Editors and Affiliations

  1. University of Southern California, Los Angeles, CA, USA

    Bistra Dilkina

Ethics declarations

Disclosure of Interests

The authors have no competing interests to declare.

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Jabs, C., Berg, J., Järvisalo, M. (2024). Core Boosting in SAT-Based Multi-objective Optimization. In: Dilkina, B. (eds) Integration of Constraint Programming, Artificial Intelligence, and Operations Research. CPAIOR 2024. Lecture Notes in Computer Science, vol 14743. Springer, Cham. https://doi.org/10.1007/978-3-031-60599-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-60599-4_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-60601-4

  • Online ISBN: 978-3-031-60599-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation