Étude des représentations booléennes pour les problèmes de sati
37
pages
Breton
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
37
pages
Breton
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
Séminaire des Doctorants Un cadre théorique et pratique commun aux formalismes SAT et CSP n-aires.Lionel Paris & Belaïd Benhamou & Pierre SiegelMardi 28 février 2006Sommaire1. Introduction et définitions préliminaires- CSP & SAT2. Relations entre SAT et CSP- Codage: direct, avec supports et k-AC3. La forme normale généralisée- définition et comparaison avec les autres transformations4. Consistance d’arc pour ce formalisme5. Algorithmes de résolutions- MAC et FC6. Résultats expérimentaux7. Conclusion28 février 2006 L. Paris - B. Benhamou - P. Siegel 21. Introduction et définitions préliminaires28 février 2006 L. Paris - B. Benhamou - P. Siegel 31. Définitions (CSP)➢ Modélisation de problèmes en IA➢ Exemple: Critères de fabrication de voitures :➢ Ensemble de variables avec leurs domaines :➢ Pare-chocs --> white➢ Toit ouvrant --> red ➢ Enjoliveurs --> pink ou red➢ Capots et Portières --> pink, red ou black➢ Carrosserie --> white, pink, red ou black➢ Contraintes du concepteur➢ Pare-chocs, toit ouvrant et enjoliveurs plus clairs que la carrosserie.➢ Portières, carrosserie et capot de la même couleur.28 février 2006 L. Paris - B. Benhamou - P. Siegel 41. Définitions (CSP)(w, p)w(w, r)PortièresPare-chocs (w, b)(r, b) w, p, r, b p, r, br p, r, bToit ouvrantCarrosserie Capot(p, p, p)(p, r)(r, r, r)(p, b)p, r (b, b, b)(r, b): plus clair queEnjoliveurs: de la même couleur que28 février 2006 L. Paris - B. Benhamou - P. Siegel 51. ...
Voir
Publié par
Langue
Breton
Séminaire des Doctorants
Un cadre théorique et pratique commun aux formalismes SAT et CSP n-aires.
Lionel Paris & Belaïd Benhamou & Pierre Siegel
Mardi 28 février 2006
Sommaire
1. Introduction et définitions préliminaires - CSP & SAT 2. Relations entre SAT et CSP - Codage: direct, avec supports etk-AC 3. La forme normale généralisée définition et comparaison avec les autres -transformations 4. Consistance d’arc pour ce formalisme 5. Algorithmes de résolutions - MAC et FC 6. Résultats expérimentaux 7. Conclusion 28 février 2006 L. Paris - B. Benhamou - P. Siegel
2
1. Introduction et définitions préliminaires
28 février 2006
L. Paris - B. Benhamou - P. Siegel
3
1. Définitions (CSP) ➢Modélisation de problèmes en IA ➢Exemple: Critères de fabrication de voitures : ➢Ensemble de variables avec leurs domaines : ➢Pare-chocs-->white ➢Toit ouvrant-->red ➢Enjoliveurs-->pink ou red ➢Capots etPortières-->pink, red ou black ➢Carrosserie-->white, pink, red ou black ➢Contraintes du concepteur ➢et enjoliveurs plus clairs que laPare-chocs, toit ouvrant carrosserie. ➢Portières, carrosserie et capot de la même couleur. 28 février 2006 L. Paris - B. Benhamou - P. Siegel 4
1. Définitions (CSP)
w Pare-chocs
r(r, b)
Toit ouvrant
p, r Enjoliveurs
28 février 2006
(w, p) (w, r)
(w, r) (w, b)
(p, r) (p, b) (r, b)
w, p, r, b
Carrosserie
Portières
p, r, b
(p, p, p) (r, r, r) (b, b, b)
: plus clair que : de la même couleur que L. Paris - B. Benhamou - P. Siegel
p, r, b
Capot
5
1. Définitions (CSP)
➢
➢
➢
CSPP= (X,D,C,R) ➢Xvariables ➢Ddomaines ➢ Ccontraintes ➢Rrelations de compatibilité Instanciation = affectation des variables du CSP à une des valeurs de leurs domaines Solution = affectation totale consistante
28 février 2006
L. Paris - B. Benhamou - P. Siegel
6
w,p,r, b
(p, r) (p, b) (r, b)
(r, b)
7
L. Paris - B. Benhamou - P. Siegel
r
(w, r) (w, b)
(w, p) (w, r)
rusilev ouvToitEnjorant
Carrosserie
(p, p, p) (r, r, r) (b, b, b)
Capot
p, r, b
Portières
p, r, b
’d e crasisncnat]:ik[F70e r w,phocsre-cPa82f véir600 2er Déf1.oisnniti)PoC( SC
1. Définitions (SAT)
➢Logique propositionnelle classique : ➢Un ensembleVde variables propositionnelles ➢Les connecteursØ(non),Ù(et),Ú(ou)
➢Formulef= combinaison de variables et de connecteurs ➢Interprétation = fonctionI:V 0, 1 } { ➢Modèle def= interprétationItelle queI[f] = 1. ➢Forme CNF :conjonction de disjonctions de littéraux
28 février 2006
L. Paris - B. Benhamou - P. Siegel
8
2. Relations entre SAT et CSP
28 février 2006
L. Paris - B. Benhamou - P. Siegel
9
2. Relations entre SAT et CSP
➢ ➢ ➢
➢
2 problèmes NP-complets Similitudes des algorithmes de résolutions Transformations CSP SAT ➢Le codage direct [De Kleer 89] ➢Le codage avec support (AC-encoding) [Kasif 90] CSP binaires. Consistance d’arc. ➢Le codagek-AC [Bessière et al. 03] CSP n-aires. K consistance relationnelle. Transformation SAT CSP [Bennaceur 96]
28 février 2006
L. Paris - B. Benhamou - P. Siegel
10
3. La forme normale généralisée
28 février 2006
L. Paris - B. Benhamou - P. Siegel
11
