Document Open Access Logo

From Crossing-Free Resolution to Max-SAT Resolution

Authors Mohamed Sami Cherif , Djamal Habet, Matthieu Py

PDF
Thumbnail PDF

File

LIPIcs.CP.2022.12.pdf
  • Filesize: 0.67 MB
  • 17 pages

Document Identifiers

Author Details

Mohamed Sami Cherif
  • Aix-Marseille Univ, Université de Toulon, CNRS, LIS, France
Djamal Habet
  • Aix-Marseille Univ, Université de Toulon, CNRS, LIS, France
Matthieu Py
  • Aix-Marseille Univ, Université de Toulon, CNRS, LIS, France

Cite AsGet BibTex

Mohamed Sami Cherif, Djamal Habet, and Matthieu Py. From Crossing-Free Resolution to Max-SAT Resolution. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CP.2022.12

Abstract

Adapting a SAT resolution proof into a Max-SAT resolution proof without considerably increasing its size is an open problem. Read-once resolution, where each clause is used at most once in the proof, represents the only fragment of resolution for which an adaptation using exclusively Max-SAT resolution is known and trivial. Proofs containing non read-once clauses are difficult to adapt because the Max-SAT resolution rule replaces the premises by the conclusions. This paper contributes to this open problem by defining, for the first time since the introduction of Max-SAT resolution, a new fragment of resolution whose proofs can be adapted to Max-SAT resolution proofs without substantially increasing their size. In this fragment, called crossing-free resolution, non read-once clauses are used independently to infer new information thus enabling to bring along each non read-once clause while unfolding the proof until a substitute is required.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • Satisfiability
  • Proof
  • Max-SAT Resolution

Metrics

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

References

  1. André Abramé and Djamal Habet. Ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver. J. Satisf. Boolean Model. Comput., 9(1):89-128, 2014. URL: https://doi.org/10.3233/sat190104.
  2. 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.
  3. Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins, editors. MaxSAT Evaluation 2021: Solver and Benchmark Descriptions. Department of Computer Science Report Series B. Department of Computer Science, University of Helsinki, Finland, 2021. URL: https://maxsat-evaluations.github.io/2021/.
  4. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum Satisfiability, pages 929-991. Frontiers in Artificial Intelligence and Applications. IOS PRESS, Netherlands, 2 edition, 2021. URL: https://doi.org/10.3233/FAIA201008.
  5. Maria Luisa Bonet and Jordi Levy. Equivalence Between Systems Stronger Than Resolution. 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 166-181. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_13.
  6. 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.
  7. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for Max-SAT. Artif. Intell., 171(8-9):606-618, 2007. URL: https://doi.org/10.1016/j.artint.2007.03.001.
  8. Joshua Buresh-Oppenheim and Toniann Pitassi. The Complexity of Resolution Refinements. J. Symb. Log., 72(4):1336-1352, 2007. URL: https://doi.org/10.2178/jsl/1203350790.
  9. Sam Buss and Jan Johannsen. On Linear Resolution. J. Satisf. Boolean Model. Comput., 10(1):23-35, 2016. URL: https://doi.org/10.3233/sat190112.
  10. Mohamed Sami Cherif, Djamal Habet, and André Abramé. Understanding the power of Max-SAT resolution through UP-resilience. Artif. Intell., 289:103397, 2020. URL: https://doi.org/10.1016/j.artint.2020.103397.
  11. Yuval Filmus, Meena Mahajan, Gaurav Sood, and Marc Vinyals. MaxSAT Resolution and Subcube Sums. 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 295-311. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_21.
  12. Federico Heras and João Marques-Silva. Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms. In Toby Walsh, editor, IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, pages 572-577. IJCAI/AAAI, 2011. URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-103.
  13. Kazuo Iwama and Eiji Miyano. Intractability of Read-Once Resolution. In Proceedings of the Tenth Annual Structure in Complexity Theory Conference, Minneapolis, Minnesota, USA, June 19-22, 1995, pages 29-36. IEEE Computer Society, 1995. URL: https://doi.org/10.1109/SCT.1995.514725.
  14. Adrian Kügel. Improved Exact Solver for the Weighted MAX-SAT Problem. In Daniel Le Berre, editor, POS-10. Pragmatics of SAT, Edinburgh, UK, July 10, 2010, volume 8 of EPiC Series in Computing, pages 15-27. EasyChair, 2010. URL: https://doi.org/10.29007/38lm.
  15. Sukhamay Kundu. Tree resolution and generalized semantic tree. In Zbigniew W. Ras and Maria Zemankova, editors, Proceedings of the ACM SIGART International Symposium on Methodologies for Intelligent Systems, ISMIS 1986, Knoxville, Tennessee, USA, October 22-24, 1986, pages 270-278. ACM, 1986. URL: https://doi.org/10.1145/12808.12838.
  16. Javier Larrosa and Federico Heras. Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In Leslie Pack Kaelbling and Alessandro Saffiotti, editors, IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30 - August 5, 2005, pages 193-198. Professional Book Center, 2005. URL: http://ijcai.org/Proceedings/05/Papers/0360.pdf.
  17. Javier Larrosa, Federico Heras, and Simon de Givry. A logical approach to efficient Max-SAT solving. Artif. Intell., 172(2-3):204-233, 2008. URL: https://doi.org/10.1016/j.artint.2007.05.006.
  18. Javier Larrosa and Emma Rollon. Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems. 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 218-232. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_16.
  19. Chu Min Li, Felip Manyà, and Jordi Planes. New Inference Rules for Max-SAT. J. Artif. Intell. Res., 30:321-359, 2007. URL: https://doi.org/10.1613/jair.2215.
  20. Chu Min Li, Felip Manyà, and Joan Ramon Soler. A Clause Tableau Calculus for MaxSAT. In Subbarao Kambhampati, editor, Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pages 766-772. IJCAI/AAAI Press, 2016. URL: http://www.ijcai.org/Abstract/16/114.
  21. Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining Clause Learning and Branch and Bound for MaxSAT. In Laurent D. Michel, editor, 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021, volume 210 of LIPIcs, pages 38:1-38:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.38.
  22. D. W. Loveland. A linear format for resolution. In M. Laudet, D. Lacombe, L. Nolin, and M. Schützenberger, editors, Symposium on Automatic Demonstration, pages 147-162, Berlin, Heidelberg, 1970. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0060630.
  23. 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: https://ojs.aaai.org/index.php/AAAI/article/view/9124.
  24. Matthieu Py, Mohamed Sami Cherif, and Djamal Habet. Towards Bridging the Gap Between SAT and Max-SAT Refutations. In 32nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI, pages 137-144. IEEE, 2020. URL: https://doi.org/10.1109/ICTAI50040.2020.00032.
  25. Matthieu Py, Mohamed Sami Cherif, and Djamal Habet. A Proof Builder for Max-SAT. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 488-498. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_33.
  26. Matthieu Py, Mohamed Sami Cherif, and Djamal Habet. Computing Max-SAT Refutations using SAT Oracles. In 33rd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2021, Washington, DC, USA, November 1-3, 2021, pages 404-411. IEEE, 2021. URL: https://doi.org/10.1109/ICTAI52525.2021.00066.
  27. Matthieu Py, Mohamed Sami Cherif, and Djamal Habet. Inferring Clauses and Formulas in Max-SAT. In 33rd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2021, Washington, DC, USA, November 1-3, 2021, pages 632-639. IEEE, 2021. URL: https://doi.org/10.1109/ICTAI52525.2021.00101.
  28. John Alan Robinson. A Machine-Oriented Logic Based on the Resolution Principle. J. ACM, 12(1):23-41, 1965. URL: https://doi.org/10.1145/321250.321253.
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