2026-07-25T02:34:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16641 2024-03-06T10:57:56Z ddc:004 open_access

From Crossing-Free Resolution to Max-SAT Resolution Cherif, Mohamed Sami Habet, Djamal Py, Matthieu Satisfiability Proof Max-SAT Resolution 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mohamed Sami Cherif and Djamal Habet and Matthieu Py 2022 Is Part Of LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2022.12 urn:nbn:de:0030-drops-166412 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2022.12 eng https://creativecommons.org/licenses/by/4.0/legalcode