Skip to Main content Skip to Navigation
Conference papers

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

Mohamed Sami Cherif 1 Djamal Habet 1 Matthieu Py 1 
1 COALA - COntraintes, ALgorithmes et Applications
LIS - Laboratoire d'Informatique et Systèmes
Résumé : 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.
Document type :
Conference papers
Complete list of metadata

https://hal-amu.archives-ouvertes.fr/hal-03714732
Contributor : Mohamed Sami CHERIF Connect in order to contact the contributor
Submitted on : Tuesday, July 5, 2022 - 7:19:49 PM
Last modification on : Thursday, July 7, 2022 - 6:13:22 AM

File

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

Identifiers

  • HAL Id : hal-03714732, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

12

Files downloads

2