• Doctorant:
  • Richard Ostrowski
  • Thèse soutenue le :
  • 15 déc. 2004

Résumé

Le problème de satisfiabilité (SAT) en logique propositionnelle capture l’essence de nombreux problèmes difficiles présents dans de nombreuses disciplines tels que l’intelligence artificielle, l’informatique, la recherche opérationnelle, etc. Ce problème revient à décider si une formule booléenne mise sous forme normale conjonctive est satisfaisable ou non. Ce problème est NP-Complet et est au coeur de la théorie de la complexité, où il joue un rôle fondamental. Dernièrement, de nouvelles méthodes de résolution sont apparues et semblent moins souffrir de l’explosion combinatoire en pratique sur de nombreux problèmes.

Une de nos première contribution consiste à exploiter certaines informations structurelles présentes sur de nombreuses instances. Ces informations structurelles sont le plus souvent masquées par le formalisme CNF. L’identification de ce type d’informations structurelles occupe une place prépondérante dans de nombreux domaines (e.g. CSP). Les travaux autour de ces aspects ont été moins nombreux dans le cadre du problème SAT. Différentes informations structurelles peuvent être étudiées (symétries, cardinalité, …). Nous nous sommes intéressés particulièrement aux fonctions booléennes (equivalences,“et”,“ou”) et aux relations de dépendance entre les variables. Nous proposons différentes méthodes permettant la détection de ces fonctions booléennes (recherche syntaxique, recherche sémantique). Puis discutons de leur utilisation au sein d’un solveur SAT. Nous proposons notamment d’exploiter de nouvelles formes simplifications découlant soit directement de propriétés naturelles des fonctions, soit de nouvelles propriétés. En particulier, nous proposons une généralisation du concept de clauses bloquées proposé initialement par O. Kullmann.

L’ensemble des techniques de détection d’informations structurelle, de simplifications a été implémenté. En particulier certains traitements ont été intégrés (comme pré-traitement) à un nouveau solveur appelé LSAT basée sur la procédure classique de Davis, Logemann et Loveland (DPLL). Ce solveur se montre assez performant sur de nombreuses classes d’instances.

Nous proposons ensuite une nouvelle forme d’apprentissage basée sur le principe de recherche complémentaire initialement proposé par P. Purdom. Le principe de Purdom peut être interprété comme une technique d’apprentissage, dans le sens où il est utilisé pour éviter de rencontrer les mêmes conflits. Il diffère des techniques d’apprentissage classiques par le fait que la partie redondante de l’espace de recherche est connue à l’avance (à chaque point de choix). Ceci permet d’éliminer la partie redondante de l’espace de recherche.

Enfin, nous combinons des méthodes basées sur la résolution et l’énumération dans le but de produire de nouvelles informations au cours de la recherche. Nous avons appliqué cette combinaison dans un premier temps dans le but de produire des sous-clauses en pré-traitement et avons proposé de généraliser son utilisation tout au long de la recherche afin de produire des informations valables « plus haut » dans l’arbre de recherche.

Mots-clés : propriétés structurelles, logique propositionnelle, SAT, procédure de Davis & Putnam, apprentissage