Document Open Access Logo

An Analysis of Core-Guided Maximum Satisfiability Solvers Using Linear Programming

Author George Katsirelos

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.12.pdf
  • Filesize: 0.77 MB
  • 19 pages

Document Identifiers

Author Details

George Katsirelos
  • Université Paris-Saclay, AgroParisTech, INRAE, UMR MIA Paris-Saclay, 91120, Palaiseau, France

Funding

This work has been partly funded by the "Agence nationale de la Recherche" (ANR-19-PIA3-0004 ANITI-DIL chair of Thomas Schiex).

Cite AsGet BibTex

George Katsirelos. An Analysis of Core-Guided Maximum Satisfiability Solvers Using Linear Programming. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.12

Abstract

Many current complete MaxSAT algorithms fall into two categories: core-guided or implicit hitting set. The two kinds of algorithms seem to have complementary strengths in practice, so that each kind of solver is better able to handle different families of instances. This suggests that a hybrid might match and outperform either, but the techniques used seem incompatible. In this paper, we focus on PMRES and OLL, two core-guided algorithms based on max resolution and soft cardinality constraints, respectively. We show that these algorithms implicitly discover cores of the original formula, as has been previously shown for PM1. Moreover, we show that in some cases, including unweighted instances, they compute the optimum hitting set of these cores at each iteration. We also give compact integer linear programs for each which encode this hitting set problem. Importantly, their continuous relaxation has an optimum that matches the bound computed by the respective algorithms. This goes some way towards resolving the incompatibility of implicit hitting set and core-guided algorithms, since solvers based on the implicit hitting set algorithm typically solve the problem by encoding it as a linear program.

Subject Classification

ACM Subject Classification
  • Theory of computation → Discrete optimization
  • Mathematics of computing → Combinatorial optimization
  • Theory of computation → Logic
  • Mathematics of computing → Solvers
Keywords
  • maximum satisfiability
  • core-guided solvers
  • minimum hitting set problem
  • linear programming

Metrics

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

References

  1. David Allouche, Christian Bessiere, Patrice Boizumault, Simon de Givry, Patricia Gutierrez, Jimmy H. M. Lee, Ka Lun Leung, Samir Loudni, Jean-Philippe Métivier, Thomas Schiex, and Yi Wu. Tractability-preserving transformations of global cost functions. Artif. Intell., 238:166-189, 2016. URL: https://doi.org/10.1016/j.artint.2016.06.005.
  2. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. Solving (weighted) partial maxsat through satisfiability testing. In International conference on theory and applications of satisfiability testing, pages 427-440. Springer, 2009. Google Scholar
  3. Carlos Ansótegui and Joel Gabàs. WPM3: an (in)complete algorithm for weighted partial maxsat. Artif. Intell., 250:37-57, 2017. URL: https://doi.org/10.1016/j.artint.2017.05.003.
  4. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Proceedings of the International Joint Conference on Artifical Intelligence (IJCAI), pages 399-404, 2009. Google Scholar
  5. F. Bacchus, J. Berg, M. Järvisalo, R. Martins, and A. (eds) Niskanen. MaxSAT evaluation 2022: Solver and benchmark descriptions. Technical Report vol. B-2022-2, Department of Computer Science, University of Helsinki, Helsinki, 2022. URL: http://hdl.handle.net/10138/318451.
  6. 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.
  7. 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.
  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. Jeremias Berg, Paul Saikko, and Matti Järvisalo. Improving the effectiveness of sat-based preprocessing for 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 239-245. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/040.
  10. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. A complete calculus for max-sat. 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 240-251. Springer, 2006. URL: https://doi.org/10.1007/11814948_24.
  11. M. C. Cooper, S. de Givry, M. Sanchez, T. Schiex, M. Zytnicki, and T. Werner. Soft arc consistency revisited. Artificial Intelligence, 174(7-8):449-478, May 2010. URL: https://doi.org/10.1016/j.artint.2010.02.001.
  12. 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.
  13. 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.
  14. 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.
  15. Tomás Dlask and Tomás Werner. On relation between constraint propagation and block-coordinate descent in linear programs. 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 194-210. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_12.
  16. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Proceedings of Theory and Applications of Satisfiability Testing (SAT), pages 502-518, 2003. Google Scholar
  17. Yuval Filmus, Meena Mahajan, Gaurav Sood, and Marc Vinyals. Maxsat resolution and subcube sums. ACM Trans. Comput. Logic, 24(1), January 2023. URL: https://doi.org/10.1145/3565363.
  18. 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.
  19. 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.
  20. Javier Larrosa and Federico Heras. Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30 - August 5, 2005, pages 193-198, 2005. Google Scholar
  21. Zhendong Lei, Yiyuan Wang, Shiwei Pan, Shaowei Cai, and Minghao Yin. CASHWMaxSAT-CorePlus: Solver description. Technical report, Department of Computer Science, University of Helsinki, Helsinki, 2022. URL: http://hdl.handle.net/10138/318451.
  22. 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.
  23. 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.
  24. Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided maxsat resolution. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Québec City, Québec, Canada., pages 2717-2723, 2014. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8513.
  25. Nina Narodytska and Nikolaj S. Bjørner. Analysis of core-guided maxsat using cores and correction sets. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 26:1-26:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.26.
  26. Raymond Reiter. A theory of diagnosis from first principles. Artificial Intelligence, 32(1):57-95, 1987. URL: https://doi.org/10.1016/0004-3702(87)90062-2.
  27. 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.
  28. Hanif D. Sherali and Warren P. Adams. A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems. SIAM Journal on Discrete Mathematics, 3(3):411-430, 1990. URL: https://doi.org/10.1137/0403036.
  29. Johan Thapper and Stanislav Zivný. Sherali-adams relaxations for valued csps. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part I, volume 9134 of Lecture Notes in Computer Science, pages 1058-1069. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47672-7_86.
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