Document Open Access Logo

SAT-Based Leximax Optimisation Algorithms

Authors Miguel Cabral, Mikoláš Janota , Vasco Manquinho

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.29.pdf
  • Filesize: 0.95 MB
  • 19 pages

Document Identifiers

Author Details

Miguel Cabral
  • INESC-ID, IST, University of Lisbon, Portugal
Mikoláš Janota
  • Czech Technical University in Prague, Czech Republic
Vasco Manquinho
  • INESC-ID, IST, University of Lisbon, Portugal

Funding

This work was partially supported by Portuguese national funds through FCT, under projects UIDB/50021/2020, PTDC/CCI-COM/31198/2017, PTDC/CCI-COM/32378/2017 and DSAIPA/AI/0044/2018. The results were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902. This article is part of the RICAIP project that has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 857306.

Cite AsGet BibTex

Miguel Cabral, Mikoláš Janota, and Vasco Manquinho. SAT-Based Leximax Optimisation Algorithms. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.29

Abstract

In several real-world problems, it is often the case that the goal is to optimise several objective functions. However, usually there is not a single optimal objective vector. Instead, there are many optimal objective vectors known as Pareto-optima. Finding all Pareto-optima is computationally expensive and the number of Pareto-optima can be too large for a user to analyse. A compromise can be made by defining an optimisation criterion that integrates all objective functions. In this paper we propose several SAT-based algorithms to solve multi-objective optimisation problems using the leximax criterion. The leximax criterion is used to obtain a Pareto-optimal solution with a small trade-off between the objective functions, which is suitable in problems where there is an absence of priorities between the objective functions. Experimental results on the Multi-Objective Package Upgradeability Optimisation problem show that the SAT-based algorithms are able to outperform the Integer Linear Programming (ILP) approach when using non-commercial ILP solvers. Additionally, experimental results on selected instances from the MaxSAT evaluation adapted to the multi-objective domain show that our approach outperforms the ILP approach using commercial solvers.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Optimization algorithms
Keywords
  • Multi-Objective Optimisation
  • Leximax
  • Sorting Networks

Metrics

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

Supplementary Materials

References

  1. Ignasi Abío, Valentin Mayer-Eichberger, and Peter J. Stuckey. Encoding linear constraints into SAT. CoRR, 2020. URL: http://arxiv.org/abs/2005.02073.
  2. Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Valentin Mayer-Eichberger. A New Look at BDDs for Pseudo-Boolean Constraints. Journal Artificial Intelligence Research, 45:443-480, 2012. Google Scholar
  3. Fadi A Aloul, Arathi Ramani, Igor Markov, and Karem Sakallah. PBS: a backtrack-search pseudo-boolean solver and optimizer. In Proceedings of the 5th International Symposium on Theory and Applications of Satisfiability, pages 346-353, 2002. Google Scholar
  4. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. Solving (weighted) partial maxsat through satisfiability testing. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 427-440. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_39.
  5. Josep Argelich, Daniel Le Berre, Inês Lynce, João P. Marques Silva, and Pascal Rapicault. Solving linux upgradeability problems using boolean optimization. In Inês Lynce and Ralf Treinen, editors, Proceedings First International Workshop on Logics for Component Configuration, LoCoCo 2010, Edinburgh, UK, 10th July 2010, volume 29 of EPTCS, pages 11-22, 2010. URL: https://doi.org/10.4204/EPTCS.29.2.
  6. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality Networks: a theoretical and empirical study. Constraints, 16(2):195-221, 2011. Google Scholar
  7. asprin webpage. URL: https://potassco.org/asprin/.
  8. 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, Frontiers in Artificial Intelligence and Applications, pages 929-991. IOS PRESS, Netherlands, 2 edition, 2021. URL: https://doi.org/10.3233/FAIA201008.
  9. Olivier Bailleux and Yacine Boufkhad. Efficient CNF Encoding of Boolean Cardinality Constraints. In Principles and Practice of Constraint Programming, volume 2833 of LNCS, pages 108-122. Springer, 2003. Google Scholar
  10. Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel. A Translation of Pseudo Boolean Constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):191-200, 2006. Google Scholar
  11. Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel. New encodings of pseudo-boolean constraints into cnf. In International Conference on Theory and Applications of Satisfiability Testing, pages 181-194. Springer, 2009. Google Scholar
  12. Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel. New Encodings of Pseudo-Boolean Constraints into CNF. In International Conference on Theory and Applications of Satisfiability Testing, volume 5584 of LNCS, pages 181-194. Springer, 2009. Google Scholar
  13. K.E. Batcher. Sorting networks and their applications. Proceedings of AFIPS Spring Joint Computer Conference, 32:307-314, 1968. Google Scholar
  14. 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.
  15. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020, 2020. Google Scholar
  16. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009. Google Scholar
  17. Boolean Leximax Optimisation solver based on iterative SAT solving, source code. URL: https://github.com/miguelcabral/leximaxIST.
  18. Sylvain Bouveret and Michel Lemaître. Computing leximin-optimal solutions in constraint networks. Artificial Intelligence, 173(2):343-364, 2009. Google Scholar
  19. Gerhard Brewka, James Delgrande, Javier Romero, and Torsten Schaub. asprin: Customizing answer set preferences without a headache. AAAI, 2015. Google Scholar
  20. Cbc solver webpage. URL: https://github.com/coin-or/Cbc.
  21. CPLEX Optimizer, IBM webpage. URL: https://www.ibm.com/analytics/cplex-optimizer.
  22. 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.
  23. 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.
  24. K. Deb, S. Agrawal, A. Pratap, and T. Meyarivan. A Fast Elitist Non-dominated Sorting Genetic Algorithm for Multi-objective Optimisation: NSGA-II. In International Conference on Parallel Problem Solving from Nature, pages 849-858. Springer, 2000. Google Scholar
  25. Detailed experimental results of the experimental evaluation on the package upgradeability problem. URL: https://sat.inesc-id.pt/~mcabral/tables/detailed/.
  26. Roberto Di Cosmo, Berke Durak, Xavier Leroy, Fabio Mancinelli, and Jérôme Vouillon. Maintaining large software distributions: new challenges from the FOSS era. In Proceedings of the FRCSS 2006 workshop, 2006. EASST Newsletter. Google Scholar
  27. Niklas Eén and Niklas Sörensson. Translating pseudo-boolean constraints into SAT. J. Satisf. Boolean Model. Comput., 2(1-4):1-26, 2006. URL: https://doi.org/10.3233/sat190014.
  28. Matthias Ehrgott. Multicriteria Optimization. Springer-Verlag, Berlin, Heidelberg, 2005. Google Scholar
  29. Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121 of Lecture Notes in Computer Science, pages 252-265. Springer, 2006. URL: https://doi.org/10.1007/11814948_25.
  30. Gerald Gamrath, Daniel Anderson, Ksenia Bestuzheva, Wei-Kun Chen, Leon Eifler, Maxime Gasse, Patrick Gemander, Ambros Gleixner, Leona Gottwald, Katrin Halbig, Gregor Hendel, Christopher Hojny, Thorsten Koch, Pierre Le Bodic, Stephen J. Maher, Frederic Matter, Matthias Miltenberger, Erik Mühmer, Benjamin Müller, Marc E. Pfetsch, Franziska Schlösser, Felipe Serrano, Yuji Shinano, Christine Tawfik, Stefan Vigerske, Fabian Wegscheider, Dieter Weninger, and Jakob Witzig. The SCIP Optimization Suite 7.0. Technical report, Optimization Online, March 2020. URL: http://www.optimization-online.org/DB_HTML/2020/03/7705.html.
  31. Martin Gebser, Roland Kaminski, and Torsten Schaub. aspcud: A linux package configuration tool based on answer set programming. Electronic Proceedings in Theoretical Computer Science, 65, September 2011. URL: https://doi.org/10.4204/EPTCS.65.2.
  32. GLPK (GNU Linear Programming Kit) webpage. URL: https://www.gnu.org/software/glpk/.
  33. Andreia P. Guerreiro, Vasco M. Manquinho, and José Rui Figueira. Exact hypervolume subset selection through incremental computations. Comput. Oper. Res., 136:105471, 2021. URL: https://doi.org/10.1016/j.cor.2021.105471.
  34. Gurobi webpage. URL: https://www.gurobi.com/.
  35. Gustavo Guttierez, Mikoláš Janota, Inês Lynce, Olivier Lhomme, Vasco Manquinho, João Marques-Silva, and Claude Michel. Mancoosi deliverable 4.3: Final version of the optimization algorithms and tools. Technical report, Mancoosi, 2011. URL: https://www.mancoosi.org/reports/d4.3.pdf.
  36. C. Henard, M. Papadakis, M. Harman, and Y. Le Traon. Combining Multi-Objective Search and Constraint Solving for Configuring Large Software Product Lines. In International Conference on Software Engineering, pages 517-528, 2015. Google Scholar
  37. Steffen Hölldobler, Norbert Manthey, and Peter Steinke. A compact encoding of pseudo-boolean constraints into SAT. In KI 2012: Advances in Artificial Intelligence, volume 7526 of LNCS, pages 107-118. Springer, 2012. Google Scholar
  38. Alexey Ignatiev, Mikolás Janota, and João Marques-Silva. Towards efficient optimization in package management systems. In Pankaj Jalote, Lionel C. Briand, and André van der Hoek, editors, 36th International Conference on Software Engineering, ICSE '14, Hyderabad, India - May 31 - June 07, 2014, pages 745-755. ACM, 2014. URL: https://doi.org/10.1145/2568225.2568306.
  39. Mikolás Janota, Inês Lynce, Vasco M. Manquinho, and João Marques-Silva. Packup: Tools for package upgradability solving. J. Satisf. Boolean Model. Comput., 8(1/2):89-94, 2012. URL: https://doi.org/10.3233/sat190090.
  40. Mikolás Janota, António Morgado, José Fragoso Santos, and Vasco M. Manquinho. The seesaw algorithm: Function optimization using 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 31:1-31:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.31.
  41. Mikoláš Janota, Inês Lynce, Vasco Manquinho, and Joao Marques-Silva. PackUp: Tools for Package Upgradability Solving: System description. Journal on Satisfiability, Boolean Modeling and Computation, 8, January 2012. URL: https://doi.org/10.3233/SAT190090.
  42. Saurabh Joshi, Ruben Martins, and Vasco M. 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.
  43. D.E. Knuth. The Art of Computer Programming: Fundamental algorithms. Number vol. 1 in Addison-Wesley series in computer science and information processing. Addison-Wesley, 1997. Google Scholar
  44. Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa. Qmaxsat: A partial max-sat solver system description. Journal on Satisfiability, Boolean Modeling and Computation, 8, 2012. URL: https://doi.org/10.3233/SAT190091.
  45. Daniel Le Berre and Anne Parrain. The sat4j library, release 2.2. Journal on Satisfiability Boolean Modeling and Computation, 7:59-64, July 2010. URL: https://doi.org/10.3233/SAT190075.
  46. Rui Li, Qinghua Zheng, Xiuqi Li, and Zheng Yan. Multi-objective optimization for rebalancing virtual machine placement. Future Gener. Comput. Syst., 105:824-842, 2020. URL: https://doi.org/10.1016/j.future.2017.08.027.
  47. lpsolve webpage. URL: https://sourceforge.net/projects/lpsolve/.
  48. Benchmarks from the Mancoosi International Solver Competition 2011. URL: http://data.mancoosi.org/misc2011/problems/.
  49. Mancoosi international solver competition 2011. URL: https://www.mancoosi.org/misc-2011/index.html.
  50. Rafael Marques, Luís M. S. Russo, and Nuno Roma. Flying tourist problem: Flight time and cost minimization in complex routes. Expert Syst. Appl., 130:172-187, 2019. URL: https://doi.org/10.1016/j.eswa.2019.04.024.
  51. João Marques-Silva and Jordi Planes. On using unsatisfiability for solving maximum satisfiability. CoRR, abs/0712.1097, 2007. URL: http://arxiv.org/abs/0712.1097.
  52. João Marques-Silva, Josep Argelich, Ana Graça, and Inês Lynce. Boolean lexicographic optimization: Algorithms & applications. Ann. Math. Artif. Intell., 62:317-343, July 2011. URL: https://doi.org/10.1007/s10472-011-9233-2.
  53. Ruben Martins, Saurabh Joshi, Vasco M. 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, 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.
  54. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Open-wbo: A modular maxsat solver,. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 438-445. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_33.
  55. MaxSAT Evaluation 2021. URL: https://maxsat-evaluations.github.io/2021/.
  56. mccs package upgradeability solver webpage. URL: https://www.i3s.unice.fr/~cpjm/misc/mccs.html.
  57. Claude Michel and Michel Rueher. Handling software upgradeability problems with MILP solvers. In Inês Lynce and Ralf Treinen, editors, Proceedings First International Workshop on Logics for Component Configuration, LoCoCo 2010, Edinburgh, UK, 10th July 2010, volume 29 of EPTCS, pages 1-10, 2010. URL: https://doi.org/10.4204/EPTCS.29.1.
  58. António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and João Marques-Silva. Iterative and core-guided maxsat solving: A survey and assessment. Constraints An Int. J., 18(4):478-534, 2013. URL: https://doi.org/10.1007/s10601-013-9146-2.
  59. Multi-Objective Boolean Optimisation benchmarks generated from the unweighted track of the MaxSAT Evaluation 2021. URL: https://sat.inesc-id.pt/~mcabral/benchmarks/mse21_pbmo.zip.
  60. Alexander Nadel. On optimizing a generic function in SAT. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pages 205-213. IEEE, 2020. URL: https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_28.
  61. Alexander Nadel and Vadim Ryvchin. Bit-Vector Optimization. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, volume 9636 of Lecture Notes in Computer Science, pages 851-867. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_53.
  62. Toru Ogawa, YangYang Liu, Ryuzo Hasegawa, Miyuki Koshimura, and Hiroshi Fujita. Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers. In International Conference on Tools with Artificial Intelligence, pages 9-17. IEEE, 2013. Google Scholar
  63. Open-WBO source code. URL: https://github.com/sat-group/open-wbo.
  64. packup package upgradeability solver webpage. URL: http://sat.inesc-id.pt/~mikolas/sw/packup/.
  65. SCIP solver webpage. URL: https://www.scipopt.org/.
  66. Carsten Sinz. Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. In Principles and Practice of Constraint Programming, volume 3709 of LNCS, pages 827-831. Springer, 2005. Google Scholar
  67. T. Soh, M. Banbara, N. Tamura, and D. Le Berre. Solving Multiobjective Discrete Optimization Problems with Propositional Minimal Model Generation. In International Conference on Principles and Practice of Constraint Programming, pages 596-614. Springer, 2017. Google Scholar
  68. Miguel Terra-Neves, Inês Lynce, and Vasco Manquinho. Introducing pareto minimal correction subsets. Proceedings of the Twentieth International Conference Theory and Applications of Satisfiability Testing, pages 195-211, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_13.
  69. Y. Xiang, Y. Zhou, Z. Zheng, and M. Li. Configuring Software Product Lines by Combining Many-Objective Optimization and SAT Solvers. ACM Transactions on Software Engineering and Methodology, 26(4):14:1-14:46, 2018. Google Scholar
  70. Yuan Yuan and Wolfgang Banzhaf. ARJA: automated repair of java programs via multi-objective genetic programming. IEEE Trans. Software Eng., 46(10):1040-1067, 2020. URL: https://doi.org/10.1109/TSE.2018.2874648.
  71. Q. Zhang and H. Li. MOEA/D: A Multiobjective Evolutionary Algorithm Based on Decomposition. IEEE Transactions on Evolutionary Computation, 11(6):712-731, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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