Une autre conversion de SAT vers CSP - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2005

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.
Fichier principal
Vignette du fichier
3.pdf (123.41 Ko) Télécharger le fichier
Loading...

Dates et versions

inria-00000045 , version 1 (24-05-2005)

Identifiants

  • HAL Id : inria-00000045 , version 1

Citer

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, France. pp.49-58. ⟨inria-00000045⟩
95 Consultations
438 Téléchargements

Partager

Gmail Facebook X LinkedIn More