Skip to Main content Skip to Navigation
New interface
Conference papers

Computing Max-SAT Refutations using SAT Oracles

Matthieu Py 1 Mohamed Sami Cherif 1 Djamal Habet 1 
1 COALA - COntraintes, ALgorithmes et Applications
LIS - Laboratoire d'Informatique et Systèmes
Abstract : Adapting a resolution refutation for SAT into a Max-SAT resolution refutation without increasing considerably the size of the refutation is an open question. This paper contributes to this topic by introducing an algorithm, called substitute generation, able to adapt any resolution refutation to get a Max-SAT refutation using SAT oracles. This algorithm is able to efficiently adapt k-stacked diamond patterns, whose transformation is exponential in the literature.
Document type :
Conference papers
Complete list of metadata

https://hal-amu.archives-ouvertes.fr/hal-03737738
Contributor : Matthieu Py Connect in order to contact the contributor
Submitted on : Monday, July 25, 2022 - 1:16:45 PM
Last modification on : Saturday, September 3, 2022 - 3:51:41 AM
Long-term archiving on: : Wednesday, October 26, 2022 - 6:19:54 PM

File

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

Identifiers

  • HAL Id : hal-03737738, version 1

Collections

Citation

Matthieu Py, Mohamed Sami Cherif, Djamal Habet. Computing Max-SAT Refutations using SAT Oracles. International Conference on Tools with Artificial Intelligence (ICTAI), Nov 2021, Visioconférence, France. ⟨hal-03737738⟩

Share

Metrics

Record views

13

Files downloads

7