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

Paulin Paris

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

Informations

• Publié par: Kocuj
• Nombre de lectures: 59
• Langue: Breton

Extrait

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  ouvToit Enjo rant

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 ,p hocsre-cPa 82f véir600 2er  Déf1.oisnniti)P oC ( 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