Document Open Access Logo

Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization

Authors Christoph Jabs , Jeremias Berg , Hannes Ihalainen , Matti Järvisalo

PDF
Thumbnail PDF

File

LIPIcs.CP.2023.18.pdf
  • Filesize: 1.47 MB
  • 20 pages

Document Identifiers

Author Details

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

Funding

Work financially supported by Academy of Finland under grants 322869, 342145 and 356046.

Acknowledgements

The authors wish to thank the Finnish Computing Competence Infrastructure (FCCI) for supporting this project with computational and data storage resources.

Cite AsGet BibTex

Christoph Jabs, Jeremias Berg, Hannes Ihalainen, and Matti Järvisalo. Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CP.2023.18

Abstract

Building on Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT) solving algorithms, several approaches to computing Pareto-optimal MaxSAT solutions under multiple objectives have been recently proposed. However, preprocessing in (Max)SAT-based multi-objective optimization remains so-far unexplored. Generalizing clause redundancy to the multi-objective setting, we establish provably-correct liftings of MaxSAT preprocessing techniques for multi-objective MaxSAT in terms of computing Pareto-optimal solutions. We also establish preservation of Pareto-MCSes - the multi-objective lifting of minimal correction sets tightly connected to optimal MaxSAT solutions - as a distinguishing feature between different redundancy notions in the multi-objective setting. Furthermore, we provide a first empirical evaluation of the effect of preprocessing on instance sizes and multi-objective MaxSAT solvers.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorial optimization
  • Theory of computation → Constraint and logic programming
Keywords
  • maximum satisfiability
  • multi-objective combinatorial optimization
  • preprocessing
  • redundancy

Metrics

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

Supplementary Materials

References

  1. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiabiliy. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of FAIA, chapter 24, pages 929-991. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201008.
  2. Olivier Bailleux and Yacine Boufkhad. Efficient CNF encoding of boolean cardinality constraints. In Francesca Rossi, editor, Principles and Practice of Constraint Programming - 9th International Conference, CP, volume 2833 of LNCS, pages 108-122. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45193-8_8.
  3. Anton Belov, António Morgado, and João Marques-Silva. SAT-based preprocessing for MaxSAT. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR, volume 8312 of LNCS, pages 96-111. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-45221-5_7.
  4. Jeremias Berg and Matti Järvisalo. Unifying reasoning and core-guided search for maximum satisfiability. In Francesco Calimeri, Nicola Leone, and Marco Manna, editors, Logics in Artificial Intelligence - 16th European Conference, JELIA, volume 11468 of LNCS, pages 287-303. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-19570-0_19.
  5. 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, 22nd European Conference on Artificial Intelligence, ECAI 2016, volume 285 of FAIA, pages 630-638. IOS Press, 2016. URL: https://doi.org/10.3233/978-1-61499-672-9-630.
  6. Pierre Bieber, Remi Delmas, and Christel Seguin. DALculus - Theory and tool for development assurance level allocation. In Francesco Flammini, Sandro Bologna, and Valeria Vittorini, editors, Computer Safety, Reliability, and Security - 30th International Conference, SAFECOMP, volume 6894 of LNCS, pages 43-56. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24270-0_4.
  7. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of FAIA. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  8. Armin Biere, Matti Järvisalo, and Benjamin Kiesl. Preprocessing in SAT solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of FAIA, chapter 9, pages 391-435. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200992.
  9. Ronen I. Brafman. A simplifier for propositional formulas with many binary clauses. IEEE Trans. Syst. Man Cybern. Part B, 34(1):52-59, 2004. URL: https://doi.org/10.1109/TSMCB.2002.805807.
  10. Miguel Cabral, Mikolás Janota, and Vasco M. 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, 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 M. 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, volume 13994 of LNCS, pages 55-73. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_7.
  12. 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, volume 3569 of LNCS, pages 61-75. Springer, 2005. URL: https://doi.org/10.1007/11499107_5.
  13. Niklas Eén and Niklas Sörensson. Temporal induction by incremental SAT solving. In Ofer Strichman and Armin Biere, editors, First International Workshop on Bounded Model Checking, BMC@CAV, volume 89 of Electronic Notes in Theoretical Computer Science, pages 543-560. Elsevier, 2003. URL: https://doi.org/10.1016/S1571-0661(05)82542-3.
  14. Matthias Ehrgott. Efficiency and nondominance. In Multicriteria Optimization (2. ed.), chapter 2, pages 23-64. Springer, 2005. Google Scholar
  15. Matthias Ehrgott. Multiobjective combinatorial optimization. In Multicriteria Optimization (2. ed.), chapter 8, pages 197-220. Springer, 2005. Google Scholar
  16. Matthias Ehrgott. Other definitions of optimality - nonscalarizing methods. In Multicriteria Optimization (2. ed.), chapter 5, pages 127-150. Springer, 2005. Google Scholar
  17. Matthias Ehrgott and Xavier Gandibleux. A survey and annotated bibliography of multiobjective combinatorial optimization. OR Spectr., 22(4):425-460, 2000. URL: https://doi.org/10.1007/s002910000046.
  18. Jon William Freeman. Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, University of Pennsylvania, USA, 1995. UMI Order No. GAX95-32175. Google Scholar
  19. James F. Gimpel. A reduction technique for prime implicant tables. In 5th Annual Symposium on Switching Circuit Theory and Logical Design, SWCT, pages 183-191. IEEE Computer Society, 1964. URL: https://doi.org/10.1109/SWCT.1964.4.
  20. Andreia P. Guerreiro, João Cortes, Daniel Vanderpooten, Cristina Bazgan, Inês Lynce, Vasco M. Manquinho, and José Rui Figueira. Exact and approximate determination of the pareto front using minimal correction subsets. Comput. Oper. Res., 153:106153, 2023. URL: https://doi.org/10.1016/j.cor.2023.106153.
  21. Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, and Armin Biere. Clause elimination for SAT and QSAT. J. Artif. Intell. Res., 53:127-168, 2015. URL: https://doi.org/10.1613/jair.4694.
  22. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. J. Autom. Reason., 64(3):533-554, 2020. URL: https://doi.org/10.1007/s10817-019-09516-0.
  23. 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.
  24. 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, volume 13385 of LNCS, pages 75-94. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_6.
  25. Christoph Jabs, Jeremias Berg, Andreas Niskanen, and Matti Järvisalo. MaxSAT-based bi-objective boolean optimization. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT, volume 236 of LIPIcs, pages 12:1-12:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.12.
  26. 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.
  27. 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, volume 6015 of LNCS, pages 129-144. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_10.
  28. Matti Järvisalo, Armin Biere, and Marijn Heule. Simulating circuit-level simplifications on CNF. J. Autom. Reason., 49(4):583-619, 2012. URL: https://doi.org/10.1007/s10817-011-9239-9.
  29. Matti Järvisalo, Marijn Heule, and Armin Biere. Inprocessing rules. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning - 6th International Joint Conference, IJCAR, volume 7364 of LNCS, pages 355-370. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31365-3_28.
  30. 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, volume 9255 of LNCS, pages 200-209. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23219-5_15.
  31. 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 - 20th International Conference, SAT, volume 10491 of LNCS, pages 449-456. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_28.
  32. 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, 7th International Workshop on First-Order Theorem Proving, FTP, volume 556 of CEUR Workshop Proceedings. CEUR-WS.org, 2009. URL: http://ceur-ws.org/Vol-556/paper06.pdf.
  33. Oliver Kullmann. On a generalization of extended resolution. Discret. Appl. Math., 96-97:149-176, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00037-2.
  34. Daniel Le Berre. Exploiting the real power of unit propagation lookahead. Electron. Notes Discret. Math., 9:59-80, 2001. URL: https://doi.org/10.1016/S1571-0653(04)00314-2.
  35. Chu Min Li. Integrating equivalency reasoning into davis-putnam procedure. In Henry A. Kautz and Bruce W. Porter, editors, Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence, pages 291-296. AAAI Press / The MIT Press, 2000. URL: http://www.aaai.org/Library/AAAI/2000/aaai00-045.php.
  36. Mark H. Liffiton and Karem A. Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason., 40(1):1-33, 2008. Google Scholar
  37. Dmitry Malioutov and Kuldeep S. Meel. MLIC: A maxsat-based framework for learning interpretable classification rules. In John N. Hooker, editor, Principles and Practice of Constraint Programming - 24th International Conference, CP, volume 11008 of LNCS, pages 312-327. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98334-9_21.
  38. 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 - 8th International Conference, CP, volume 2470 of LNCS, pages 185-199. Springer, 2002. URL: https://doi.org/10.1007/3-540-46135-3_13.
  39. Tobias Paxian, Pascal Raiola, and Bernd Becker. On preprocessing for weighted MaxSAT. In Verification, Model Checking, and Abstract Interpretation, VMCAI, volume 12597 of LNCS, pages 556-577. Springer, 2021. Google Scholar
  40. 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, volume 10416 of LNCS, pages 596-614. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_38.
  41. Sathiamoorthy Subbarayan and Dhiraj K. Pradhan. NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In Holger H. Hoos and David G. Mitchell, editors, Theory and Applications of Satisfiability Testing, 7th International Conference, SAT, volume 3542 of LNCS, pages 276-291. Springer, 2004. URL: https://doi.org/10.1007/11527695_22.
  42. Miguel Terra-Neves, Inês Lynce, and Vasco M. Manquinho. Introducing pareto minimal correction subsets. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - 20th International Conference, SAT, volume 10491 of LNCS, pages 195-211. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_13.
  43. Miguel Terra-Neves, Inês Lynce, and Vasco M. Manquinho. Multi-objective optimization through pareto minimal correction subsets. In Jérôme Lang, editor, 27th Joint Conference on Artificial Intelligence, IJCAI, pages 5379-5383. ijcai.org, 2018. URL: https://doi.org/10.24963/ijcai.2018/757.
  44. Ekunda L. Ulungu and Jacques Teghem. Multi-objective combinatorial optimization problems: A survey. Journal of Multi-criteria Decision Analysis, 3:83-104, 1994. Google Scholar
  45. Allen Van Gelder. Toward leaner binary-clause reasoning in a satisfiability solver. Ann. Math. Artif. Intell., 43(1):239-253, 2005. URL: https://doi.org/10.1007/s10472-005-0433-5.
  46. 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, AAAI, pages 155-160. AAAI Press / The MIT Press, 1988. URL: http://www.aaai.org/Library/AAAI/1988/aaai88-028.php.
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