LIPIcs.CP.2021.28.pdf
- Filesize: 0.89 MB
- 19 pages
Document
Refined Core Relaxation for Core-Guided MaxSAT Solving
Authors
Jeremias Berg 
,
Matti Järvisalo
-
Part of:
Volume:
27th International Conference on Principles and Practice of Constraint Programming (CP 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Principles and Practice of Constraint Programming (CP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-10-15
File
Document Identifiers
Author Details
Cite As Get BibTex
Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Refined Core Relaxation for Core-Guided MaxSAT Solving. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.28
Abstract
Maximum satisfiability (MaxSAT) is a viable approach to solving NP-hard optimization problems. In the realm of core-guided MaxSAT solving - one of the most effective MaxSAT solving paradigms today - algorithmic variants employing so-called soft cardinality constraints have proven very effective. In this work, we propose to combine weight-aware core extraction (WCE) - a recently proposed approach that enables relaxing multiple cores instead of a single one during iterations of core-guided search - with a novel form of structure sharing in the cardinality-based core relaxation steps performed in core-guided MaxSAT solvers. In particular, the proposed form of structure sharing is enabled by WCE, which has so-far not been widely integrated to MaxSAT solvers, and allows for introducing fewer variables and clauses during the MaxSAT solving process. Our results show that the proposed techniques allow for avoiding potential overheads in the context of soft cardinality constraint based core-guided MaxSAT solving both in theory and in practice. In particular, the combination of WCE and structure sharing improves the runtime performance of a state-of-the-art core-guided MaxSAT solver implementing the central OLL algorithm.
Subject Classification
ACM Subject Classification
- Mathematics of computing → Combinatorial optimization
- Theory of computation → Constraint and logic programming
Keywords
- maximum satisfiability
- MaxSAT
- core-guided MaxSAT solving
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Benjamin Andres, Benjamin Kaufmann, Oliver Matheis, and Torsten Schaub. Unsatisfiability-based optimization in CLASP. In Agostino Dovier and Vítor Santos Costa, editors, Technical Communications of the 28th International Conference on Logic Programming, ICLP 2012, September 4-8, 2012, Budapest, Hungary, volume 17 of LIPIcs, pages 211-221. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.ICLP.2012.211.
- 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.
- 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.
- Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. SAT-based MaxSAT algorithms. Artificial Intelligence, 196:77-105, 2013. URL: https://doi.org/10.1016/j.artint.2013.01.002.
- Carlos Ansótegui and Joel Gabàs. WPM3: an (in)complete algorithm for weighted partial MaxSAT. Artificial Intelligence, 250:37-57, 2017. URL: https://doi.org/10.1016/j.artint.2017.05.003.
-
Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins, editors. MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, volume B-2020-2 of Department of Computer Science Report Series B. Department of Computer Science, University of Helsinki, Finland, 2020.
- 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.
- 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, volume 336 of Frontiers in Artificial Intelligence and Applications, chapter 24, pages 929-991. IOS Press BV, 2 edition, 2021. URL: https://doi.org/10.3233/FAIA201008.
- 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.
- 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.
- Jeremias Berg and Matti Järvisalo. Weight-aware core extraction in SAT-based MaxSAT solving. In 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.
- Nikolaj Bjørner and Nina Narodytska. Maximum satisfiability using cores and correction sets. In Qiang Yang and Michael Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 246-252. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/041.
- Jori Bomanson, Martin Gebser, and Tomi Janhunen. Improving the normalization of weight rules in answer set programs. In Eduardo Fermé and João Leite, editors, Logics in Artificial Intelligence - 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings, volume 8761 of Lecture Notes in Computer Science, pages 166-180. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11558-0_12.
- 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.
- Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In Armin Biere and Carla 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.
- Federico Heras, António Morgado, and João Marques-Silva. Lower bounds and upper bounds for MaxSAT. In Youssef Hamadi and Marc Schoenauer, editors, Learning and Intelligent Optimization - 6th International Conference, LION 6, Paris, France, January 16-20, 2012, Revised Selected Papers, volume 7219 of Lecture Notes in Computer Science, pages 402-407. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-34413-8_35.
- Alexey Ignatiev, António Morgado, and João Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 428-437. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
- 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.
- Chu Min Li and Felip Manyà. MaxSAT, hard and soft constraints. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 903-927. IOS Press, 2 edition, 2021. URL: https://doi.org/10.3233/FAIA201007.
- Chu Min Li, Felip Manyà, and Jordi Planes. Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT. In Proceedings, The Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, July 16-20, 2006, Boston, Massachusetts, USA, pages 86-91. AAAI Press, 2006. URL: http://www.aaai.org/Library/AAAI/2006/aaai06-014.php.
- Vasco Manquinho, João Marques Silva, and Jordi Planes. Algorithms for weighted boolean optimization. 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 495-508. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_45.
- 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.
- 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.
- Ruben Martins, Saurabh Joshi, Vasco 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.
- Ruben Martins, Vasco 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.
- 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.
- António Morgado, Federico Heras, Mark 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.
- Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided MaxSAT resolution. In Carla 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.