Inferring Clauses and Formulas in Max-SAT

Explication de clauses et de formules dans Max-SAT

Matthieu Py (1) , Mohamed Sami Cherif (1) , Djamal Habet (1)

1 COALA - COntraintes, ALgorithmes et Applications

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.

Mots clés: Max-SAT; Proof Systems; Inference

Domaines: Informatique [cs]

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⟩