Document Open Access Logo

Analysis of Core-Guided MaxSat Using Cores and Correction Sets

Authors Nina Narodytska , Nikolaj Bjørner

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.26.pdf
  • Filesize: 1.92 MB
  • 20 pages

Document Identifiers

Author Details

Nina Narodytska
  • VMware Research, Palo Alto, CA, USA
Nikolaj Bjørner
  • Microsoft Research, Redmond, WA, USA

Cite As Get BibTex

Nina Narodytska and Nikolaj Bjørner. Analysis of Core-Guided MaxSat Using Cores and Correction Sets. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.SAT.2022.26

Abstract

Core-guided solvers are among the best performing algorithms for solving maximum satisfiability problems. These solvers perform a sequence of relaxations of the formula to increase the lower bound on the optimal solution at each relaxation step. In addition, the relaxations allow generating a large set of minimal cores (MUSes) of the original formula. However, properties of these cores in relation to the optimization objective have not been investigated. In contrast, minimum hitting set based solvers (MaxHS) extract a set of cores that are known to have properties related to the optimization objective, e.g., the size of the minimum hitting set of the discovered cores equals the optimum when the solver terminates. In this work we analyze minimal cores and minimum correction sets (MinCSes) of the input formula and its sub-formulas that core-guided solvers produce. We demonstrate that a set of MUSes that a core-guided algorithm discovers possess the same key properties as cores extracted by MaxHS solvers. For instance, we prove the size of a minimum hitting set of these cores equals the optimal cost. We also show that it discovers all MinCSes of special subformulas of the input formula. We discuss theoretical and practical implications of our results.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Mathematics of computing → Solvers
Keywords
  • maximum satisfiability
  • unsatisfiable cores
  • correction sets

Metrics

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

References

  1. Carlos Ansótegui, Maria Luisa Bonet, Joel Gabàs, and Jordi Levy. Improving WPM2 for (weighted) partial maxsat. 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 117-132. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40627-0_12.
  2. Carlos Ansótegui and Joel Gabàs. WPM3: an (in)complete algorithm for weighted partial maxsat. Artif. Intell., 250:37-57, 2017. Google Scholar
  3. Florent Avellaneda. A short description of the solver EvalMaxSAT. URL: https://maxsat-evaluations.github.io/2021/mse21-solver-src/complete/evalmaxsat.zip, 2021.
  4. 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.
  5. Fahiem Bacchus and George Katsirelos. Using minimal correction sets to more efficiently compute minimal unsatisfiable sets. In Computer Aided Verification - 27th International Conference, CAV 2015, July 18-24, 2015, volume 9207, pages 70-86, 2015. Google Scholar
  6. Fahiem Bacchus and Nina Narodytska. Cores in core based maxsat algorithms: An analysis. 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 7-15. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_2.
  7. Jeremias Berg, Fahiem Bacchus, and Alex Poole. Abstract cores in implicit hitting set maxsat solving (extended abstract). In Zhi-Hua Zhou, editor, Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 4745-4749. ijcai.org, 2021. URL: https://doi.org/10.24963/ijcai.2021/643.
  8. 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.
  9. Nikolaj Bjørner and Nina Narodytska. Maximum satisfiability using cores and correction sets. In IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 246-252, 2015. Google Scholar
  10. Shaowei Cai and Zhendong Lei. Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability. Artif. Intell., 287:103354, 2020. URL: https://doi.org/10.1016/j.artint.2020.103354.
  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. 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.
  13. 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.
  14. Zhendong Lei, Shaowei Cai, Dongxu Wang, Yongrong Peng, Fei Geng, Dongdong Wan, Yiping Deng, and Pinyan Lu. CASHWMaxSAT: Solver description, 2021. URL: https://maxsat-evaluations.github.io/2021/mse21-solver-src/complete/cashmaxsat.zip, 2021.
  15. Mark H. Liffiton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva. Fast, flexible MUS enumeration. Constraints, 21(2):223-250, 2016. Google Scholar
  16. Mark H. Liffiton and Karem A. Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning, 40(1):1-33, 2008. Google Scholar
  17. 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.
  18. Antonio Morgado, Federico Heras, Mark Liffiton, Jordi Planes, and Joao Marques-Silva. Iterative and core-guided maxsat solving: A survey and assessment. Constraints, 18(4):478-534, October 2013. URL: https://doi.org/10.1007/s10601-013-9146-2.
  19. António Morgado, Alexey Ignatiev, and João Marques-Silva. MSCG: robust core-guided maxsat solving. J. Satisf. Boolean Model. Comput., 9(1):129-134, 2014. URL: https://doi.org/10.3233/sat190105.
  20. Antonio Morgado, Mark H. Liffiton, and Joao Marques-Silva. Maxsat-based MCS enumeration. In HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers, volume 7857, pages 86-101. Springer, 2012. Google Scholar
  21. Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided maxsat resolution. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 2014., pages 2717-2723. AAAI Press, 2014. Google Scholar
  22. Nina Narodytska, Nikolaj Bjørner, Maria-Cristina V. Marinescu, and Mooly Sagiv. Core-guided minimal correction set and core enumeration. 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 1353-1361. ijcai.org, 2018. URL: https://doi.org/10.24963/ijcai.2018/188.
  23. Marek Piotrow. UWrMaxSat in maxsat evaluation 2021. URL: https://maxsat-evaluations.github.io/2021/mse21-solver-src/complete/uwrmaxsat.zip, 2021.
  24. Raymond Reiter. A theory of diagnosis from first principles. Artif. Intell., 32(1):57-95, 1987. 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 About DROPS Imprint Privacy Contact