De la résolution à la max-résolution

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

1 COALA - COntraintes, ALgorithmes et Applications

Adapter une preuve par résolution en une preuve par max-résolution sans augmenter considérablement sa taille est une question ouverte. En effet, la seule classe dont l'adaptation est connue et triviale est celle où les clauses sont utilisées au plus une fois dans les preuves. Dans ce papier, on propose une nouvelle classe de résolution, appelée résolution sans croisement, dans laquelle les clauses réutilisées plusieurs fois sont exploitées indépendemment pour générer de nouvelles informations. On démontre que les preuves de cette classe peuvent être adaptées en preuves par max-résolution sans augmentation considérable de leur taille en utilisant les clauses de compensation générées par la max-résolution.

Mots clés: Preuves; Résolution sans croisement; Max-résolution; Max-SAT

Domaines: Intelligence artificielle [cs.AI]

Mohamed Sami Cherif, Djamal Habet, Matthieu Py. De la résolution à la max-résolution. Journées Francophones de Programmation par Contraintes (JFPC), Jun 2022, Saint-Étienne, France. ⟨hal-03714732⟩