Étude des représentations booléennes pour les problèmes de sati
37 pages
Breton

Étude des représentations booléennes pour les problèmes de sati

-

Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Description

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. ...

Sujets

Informations

Publié par
Nombre de lectures 59
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