Skip to Main content Skip to Navigation
New interface
Conference papers

Inferring Clauses and Formulas in Max-SAT

Matthieu Py 1 Mohamed Sami Cherif 1 Djamal Habet 1 
1 COALA - COntraintes, ALgorithmes et Applications
LIS - Laboratoire d'Informatique et Systèmes
Abstract : In this paper, we are interested in proof systems for Max-SAT and particularly in the construction of Max-SAT equivalence-preserving transformations to infer information from a given formula. To this end, we introduce the notion of explainability and we provide a characterization for explainable clauses and formulas. Furthermore, we introduce a new proof system, called Explanation Calculus (ExC) and composed of two rules: symmetric cut and expansion. We study the relation between ExC and several existing proof systems. Then, we introduce a new algorithm, called explanation algorithm, able to construct an explanation in ExC for any clause or refute its explainability and we extend it for formula explanations. Finally, we use our results on explainability to provide proofs for the Max-SAT problem with a new bound on the number of inference steps in the proof, improving the bound obtained with the Max-SAT resolution calculus.
Document type :
Conference papers
Complete list of metadata
Contributor : Matthieu Py Connect in order to contact the contributor
Submitted on : Monday, July 25, 2022 - 1:20:33 PM
Last modification on : Saturday, September 3, 2022 - 3:51:42 AM
Long-term archiving on: : Wednesday, October 26, 2022 - 6:20:14 PM


Files produced by the author(s)


  • HAL Id : hal-03737741, version 1



Matthieu Py, Mohamed Sami Cherif, Djamal Habet. Inferring Clauses and Formulas in Max-SAT. The 33rd IEEE International Conference on Tools with Artificial Intelligence (ICTAI), Nov 2021, Vidéoconférence, France. ⟨hal-03737741⟩



Record views


Files downloads