Skip to Main content Skip to Navigation
Conference papers

Une autre conversion de SAT vers CSP

Résumé : Cet article présente une transformation d'une formule propositionnelle du problème SAT en une autre formule propositionnelle qui, à son tour, peut être directement transformée en un problème CSP binaire. Cette transformation est basée sur une procédure de recherche de modèles locaux qui est contrôlée pour obtenir une transformation qui soit globalement polynomiale. Une méthode pour réduire la taille de la formule finale est proposée. Nous montrons également que le maintien de la k-consistance sur le problème CSP est équivalent à l'utilisation de la propagation unitaire sur une forme compilée de la formule propositionnelle correspondante dans le problème SAT. De notre point de vue, cette transformation établit un autre pont naturel entre SAT et CSP qui pourrait être bénéfique aux deux communautés.
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000045
Contributor : Christine Solnon <>
Submitted on : Tuesday, May 24, 2005 - 1:14:52 PM
Last modification on : Thursday, January 11, 2018 - 6:19:28 AM
Long-term archiving on: : Thursday, April 1, 2010 - 9:30:37 PM

File

Identifiers

  • HAL Id : inria-00000045, version 1

Collections

Citation

Olivier Roussel. Une autre conversion de SAT vers CSP. Premières Journées Francophones de Programmation par Contraintes, CRIL - CNRS FRE 2499, Jun 2005, Lens, pp.49-58. ⟨inria-00000045⟩

Share

Metrics

Record views

172

Files downloads

534