Retour à l'index du GREYC

Séminaire Algorithmique

Site du CNRS

Séminaire Algorithmique

Le séminaire a lieu le mardi à 11 h 45 (sauf modification exceptionnelle), au campus Côte de Nacre, bâtiment Sciences 3, salle S3 351, 3ème étage.

Résumé du séminaire du Mardi 17 Juin 2003

Techniques d'extraction et de simplification de formules CNF

par Richard Ostrowski (CRIL université d'Artois)

La représentation des connaissances et les problèmes d'inférences associés restent à l'heure actuelle une problématique riche et centrale en Informatique et plus précisément en Intelligence Artificielle.

Le formalisme considéré est la logique propositionnelle qui permet d'allier puissance d'expression et efficacité. Il reste que la déduction en logique propositionnelle ne peut admettre de solutions à la fois générales et efficaces. Pour certaines classes de problèmes réels ou structurés, une des voies pour réduire considérablement l'espace de recherche est de prendre en compte les informations structurelles de la formule considérée. En effet la prise en compte de ce type d'information conduit souvent à une résolution plus efficace.

Après un bref rappel du problème SAT et des différents algorithmes existants, nous proposerons une technique permettant de rechercher (par abstraction) des structures particulières (équivalences,fonctions booléennes "Et" et "Ou") en vue de simplifier les formules. Ensuite nous présenterons une autre forme de simplification basée sur la notion de clauses bloquées (permettant à la fois de supprimer des clauses et des variables).

GREYC
Campus Côte de Nacre, boulevard du Maréchal Juin
BP 5186
14032 Caen Cedex
FAX : +33 (0)2 31 56 73 30
http://www.greyc.fr