Document Open Access Logo

Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights

Authors Andreas Niskanen , Jeremias Berg , Matti Järvisalo

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.44.pdf
  • Filesize: 1.39 MB
  • 19 pages

Document Identifiers

Author Details

Andreas Niskanen
  • HIIT, Department of Computer Science, University of Helsinki, Finland
Jeremias Berg
  • 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, 328718 and 342145.

Cite AsGet BibTex

Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 44:1-44:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.44

Abstract

Recent advances in solvers for the Boolean satisfiability (SAT) based optimization paradigm of maximum satisfiability (MaxSAT) have turned MaxSAT into a viable approach to finding provably optimal solutions for various types of hard optimization problems. In various types of real-world problem settings, a sequence of related optimization problems need to solved. This calls for studying ways of enabling incremental computations in MaxSAT, with the hope of speeding up the overall computation times. However, current state-of-the-art MaxSAT solvers offer no or limited forms of incrementality. In this work, we study ways of enabling incremental computations in the context of the implicit hitting set (IHS) approach to MaxSAT solving, as both one of the key MaxSAT solving approaches today and a relatively well-suited candidate for extending to incremental computations. In particular, motivated by several recent applications of MaxSAT in the context of interpretability in machine learning calling for this type of incrementality, we focus on enabling incrementality in IHS under changes to the objective function coefficients (i.e., to the weights of soft clauses). To this end, we explain to what extent different search techniques applied in IHS-based MaxSAT solving can and cannot be adapted to this incremental setting. As practical result, we develop an incremental version of an IHS MaxSAT solver, and show it provides significant runtime improvements in recent application settings which can benefit from incrementality but in which MaxSAT solvers have so-far been applied only non-incrementally, i.e., by calling a MaxSAT solver from scratch after each change to the problem instance at hand.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorial optimization
  • Theory of computation → Constraint and logic programming
Keywords
  • Constraint optimization
  • maximum satisfiability
  • MaxSAT
  • implicit hitting set approach

Metrics

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

Supplementary Materials

References

  1. Mario Alviano, Carmine Dodaro, and Francesco Ricca. A MaxSAT algorithm using cardinality constraints of bounded size. In Qiang Yang and Michael J. Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 2677-2683. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/379.
  2. Carlos Ansótegui, Frédéric Didier, and Joel Gabàs. Exploiting the structure of unsatisfiable cores in MaxSAT. In Qiang Yang and Michael J. Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 283-289. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/046.
  3. Fahiem Bacchus, Antti Hyttinen, Matti Järvisalo, and Paul Saikko. Reduced cost fixing in MaxSAT. 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 641-651. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_41.
  4. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. MaxSAT Evaluation 2018: New developments and detailed results. Journal on Satisfiability, Boolean Modeling and Computation, 11(1):99-131, 2019. URL: https://doi.org/10.3233/SAT190119.
  5. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins, editors. MaxSAT Evaluation 2019: Solver and Benchmark Descriptions, volume B-2019-2 of Department of Computer Science Report Series B. Department of Computer Science, University of Helsinki, Finland, 2019. URL: https://hdl.handle.net/10138/308068.
  6. 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, chapter 24, pages 929-991. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201008.
  7. 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.
  8. Jeremias Berg, Fahiem Bacchus, and Alex Poole. Abstract cores in implicit hitting set MaxSat solving. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 277-294. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_20.
  9. Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. A modular approach to MaxSAT modulo theories. 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 150-165. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_12.
  10. Jessica Davies. Solving MAXSAT by Decoupling Optimization and Satisfaction. PhD thesis, University of Toronto, 2013. URL: https://hdl.handle.net/1807/43539.
  11. 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.
  12. Jessica Davies and Fahiem Bacchus. Postponing optimization to speed up MAXSAT solving. In Christian Schulte, editor, Principles and Practice of Constraint Programming - 19th International Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013, Proceedings, volume 8124 of Lecture Notes in Computer Science, pages 247-262. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40627-0_21.
  13. Niklas Eén and Niklas Sörensson. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 89(4):543-560, 2003. URL: https://doi.org/10.1016/S1571-0661(05)82542-3.
  14. Yoav Freund and Robert E. Schapire. A decision-theoretic generalization of on-line learning and an application to boosting. Journal of Computer and System Sciences, 55(1):119-139, 1997. URL: https://doi.org/10.1006/jcss.1997.1504.
  15. Bishwamittra Ghosh and Kuldeep S. Meel. IMLI: an incremental framework for MaxSAT-based learning of interpretable classification rules. In Vincent Conitzer, Gillian K. Hadfield, and Shannon Vallor, editors, Proceedings of the 2019 AAAI/ACM Conference on AI, Ethics, and Society, AIES 2019, Honolulu, HI, USA, January 27-28, 2019, pages 203-210. ACM, 2019. URL: https://doi.org/10.1145/3306618.3314283.
  16. Hao Hu, Mohamed Siala, Emmanuel Hebrard, and Marie-José Huguet. Learning optimal decision trees with MaxSAT and its integration in AdaBoost. In Christian Bessiere, editor, Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, pages 1170-1176. ijcai.org, 2020. URL: https://doi.org/10.24963/ijcai.2020/163.
  17. Alexey Ignatiev, António Morgado, and João Marques-Silva. RC2: an efficient MaxSAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 11(1):53-64, 2019. URL: https://doi.org/10.3233/SAT190116.
  18. 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 2018, Lille, France, August 27-31, 2018, Proceedings, volume 11008 of Lecture Notes in Computer Science, pages 312-327. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98334-9_21.
  19. Ravi Mangal, Xin Zhang, Aditya Kamath, Aditya V. Nori, and Mayur Naik. Scaling relational inference using proofs and refutations. In Dale Schuurmans and Michael P. Wellman, editors, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA, pages 3278-3286. AAAI Press, 2016. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI16/paper/view/12466.
  20. 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 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.
  21. Ruben Martins, Saurabh Joshi, Vasco M. Manquinho, and Inês Lynce. On using incremental encodings in unsatisfiability-based MaxSAT solving. Journal on Satisfiability, Boolean Modeling and Computation, 9(1):59-81, 2014. URL: https://doi.org/10.3233/sat190102.
  22. 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.
  23. 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.
  24. 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, 18(4):478-534, 2013. URL: https://doi.org/10.1007/s10601-013-9146-2.
  25. Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided MaxSAT resolution. In Carla E. Brodley and Peter Stone, editors, Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Québec City, Québec, Canada, pages 2717-2723. AAAI Press, 2014. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8513.
  26. Nina Narodytska, Alexey Ignatiev, Filipe Pereira, and João Marques-Silva. Learning optimal decision trees with SAT. 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 1362-1368. ijcai.org, 2018. URL: https://doi.org/10.24963/ijcai.2018/189.
  27. Matthew Richardson and Pedro M. Domingos. Markov logic networks. Machine Learning, 62(1-2):107-136, 2006. URL: https://doi.org/10.1007/s10994-006-5833-1.
  28. Paul Saikko. Re-implementing and extending a hybrid SAT-IP approach to maximum satisfiability. Master’s thesis, University of Helsinki, 2015. URL: http://hdl.handle.net/10138/159186.
  29. Paul Saikko, Jeremias Berg, and Matti Järvisalo. LMHS: A SAT-IP hybrid MaxSAT solver. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, 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.
  30. Xujie Si, Xin Zhang, Vasco M. Manquinho, Mikolás Janota, Alexey Ignatiev, and Mayur Naik. On incremental core-guided MaxSAT solving. In Michel Rueher, editor, Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings, volume 9892 of Lecture Notes in Computer Science, pages 473-482. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-44953-1_30.
  31. Jinqiang Yu, Alexey Ignatiev, Pierre Le Bodic, and Peter J. Stuckey. Optimal decision lists using SAT. CoRR, abs/2010.09919, 2020. URL: http://arxiv.org/abs/2010.09919.
  32. Jinqiang Yu, Alexey Ignatiev, Peter J. Stuckey, and Pierre Le Bodic. Computing optimal decision sets with SAT. In Helmut Simonis, editor, Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings, volume 12333 of Lecture Notes in Computer Science, pages 952-970. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_55.
  33. Xin Zhang, Ravi Mangal, Aditya V. Nori, and Mayur Naik. Query-guided maximum satisfiability. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 109-122. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837658.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact