Skip to Main content Skip to Navigation
Conference papers

Towards Bridging the Gap Between SAT and Max-SAT Refutations

Matthieu Py 1 Mohamed Cherif 1 Djamal Habet 1
1 COALA - COntraintes, ALgorithmes et Applications
LIS - Laboratoire d'Informatique et Systèmes
Abstract : Adapting a resolution proof for SAT to a Max-SAT resolution proof without increasing considerably the size of the proof is an open question. This paper contributes to this topic by exhibiting linear adaptations, in terms of the input SAT proof size, in restricted cases which are regular tree resolution refutations, tree resolution refutations and a new introduced class of refutations that we refer to as semi-tree resolution refutations. We also extend these results by proposing a complete adaptation for any unrestricted SAT refutation to a Max-SAT refutation, which is exponential in the worst case.
Document type :
Conference papers
Complete list of metadatas

https://hal-amu.archives-ouvertes.fr/hal-03134416
Contributor : Matthieu Py <>
Submitted on : Monday, February 8, 2021 - 12:06:51 PM
Last modification on : Saturday, February 13, 2021 - 3:19:06 AM

File

ICTAI_2020___Towards_Bridging_...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03134416, version 1

Collections

Citation

Matthieu Py, Mohamed Cherif, Djamal Habet. Towards Bridging the Gap Between SAT and Max-SAT Refutations. 32th International Conference on Tools with Artificial Intelligence, Nov 2020, Baltimore, United States. ⟨hal-03134416⟩

Share

Metrics

Record views

31

Files downloads

14