| Title: |
From Crossing-Free Resolution to Max-SAT Resolution |
| Authors: |
Cherif, Mohamed, Sami; Habet, Djamal; Py, Matthieu |
| Contributors: |
COntraintes, ALgorithmes et Applications (COALA); Laboratoire d'Informatique et des Systèmes (LIS) (Marseille, Toulon) (LIS); Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS) |
| Source: |
28th International Conference on Principles and Practice of Constraint Programming (CP 2022); https://amu.hal.science/hal-03979371; 28th International Conference on Principles and Practice of Constraint Programming (CP 2022), Jul 2022, Haifa, Israel. ⟨10.4230/LIPIcs.CP.2022.12⟩ |
| Publisher Information: |
CCSD |
| Publication Year: |
2022 |
| Collection: |
Université de Toulon: HAL |
| Subject Terms: |
2012 ACM Subject Classification Theory of computation → Proof theory phrases Satisfiability; Satisfiability; Proofs; Max-SAT resolution; [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI] |
| Subject Geographic: |
Haifa; Israel |
| Description: |
International audience ; 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. |
| Document Type: |
conference object |
| Language: |
English |
| DOI: |
10.4230/LIPIcs.CP.2022.12 |
| Availability: |
https://amu.hal.science/hal-03979371; https://amu.hal.science/hal-03979371v1/document; https://amu.hal.science/hal-03979371v1/file/LIPIcs-CP-2022-12.pdf; https://doi.org/10.4230/LIPIcs.CP.2022.12 |
| Rights: |
info:eu-repo/semantics/OpenAccess |
| Accession Number: |
edsbas.A156B5D9 |
| Database: |
BASE |