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

Dans ce papier, on s'intéresse à la construction de transformations préservant l'équivalence Max-SAT afin d'inférer de l'information (clause ou formule) à partir d'une formule donnée. Dans ce but, on définit et caractérise la notion de clauses et formules explicables, on propose un système de preuve complet pour l'inférence dans Max-SAT et un algorithme associé pour expliquer ou réfuter l'explicabilité de n'importe quelle clause ou formule. On donne enfin des bornes théoriques sur la taille des transformations calculées. Cet article résume le travail publié à la conférence ICTAI 2021 [3].

Domains: Computer Science [cs]

Matthieu Py, Mohamed Sami Cherif, Djamal Habet. Explication de clauses et de formules dans Max-SAT. JFPC 2022, Jun 2022, Saint-Etienne, France. ⟨hal-03737733⟩