20/05/2007

Présentation du problème SAT et des techniques de résolutions

 

Le formalisme

Un problème SAT est représenté au moyen de variables propositionnelles qui peuvent prendre la valeur (faux) ou (vrai).

On appelle "littéral" une variable ou son complément .
Une "clause" est une disjonction de littéraux (par exemple ( ou ) ou encore ( ou )).
Une "formule" logique sous forme normale conjonctive (CNF) est une conjonction de clauses.

Un littéral qui a la valeur est dit satisfait. Une clause est satisfaite si l'un de ces littéraux l'est. Une formule est satisfaite si toutes ses clauses le sont.

Le problème SAT est un problème NP-complet (d'après le théorème de Cook) qui consiste à dire s'il existe ou non une combinaison de valeurs pour les littéraux d'une formule donnée, telle que ces valeurs satisfont cette formule.

 

Exemple 1

Soient des variables propositionnelles. Soit l'expression .

Pour cet exemple simple, il est possible de déterminer les valeurs de toutes les variables par simples déduction. En effet, on s'aperçoit que vaut , on peut donc déduire de et trouver que vaut . Ainsi, on peut en déduire à partir de et trouver que vaut .

Cette résolution très simple n'est bien sûr pas applicable à tous les coups. Dans l'exemple, chaque valeur des variables pouvait se déduire. Dans le cas général, il faudrait développer l'arbre de recherche.

 

Exemple 2

Ce problème consiste à déterminer s'il est possible de placer pigeons dans pigeonniers, un pigeonnier ne pouvant être occupé au plus que par un seul pigeon.

Pour modéliser ce problème, on utilise variables propositionnelles avec variant de à , et variant de à . Si est vraie alors le pigeon trouve dans le pigeonnier .

Ce problème, archétype des problèmes combinatoires, est intéressant et sa solution est évidente mais le résoudre peut demander un important temps de calcul :

 

• si , le problème est consistant et la recherche d'une solution se fait de manière linéaire sachant que le nombre de solutions () est exponentiel,
• si , le problème est inconsistant mais les algorithmes standard (du type Davis et Putnam) prouvent l'inconsistance en un temps exponentiel.

Le problème, écrit en fonction des clauses de cardinalité, s'exprime par :

 

• chaque pigeon occupe un seul pigeonnier :
  

   

  
   
  

   
  

   

• chaque pigeonnier contient au plus un pigeon :
  

   

  
  

     

  
  

   

 

Problème SAT Nombre de variables pigeons Non pigeons Non pigeons Oui

 

Quelques méthodes de résolution

 

Les méthodes de saturation

Ces méthode effectuent des tests de consistance locale pour détecter l'incohérence de la base de clauses. Elles essaient de prouver l'inconsistance de l'ensemble de clauses en réfutant (démontrant la fausseté) une d’elles.

On pourra notamment citer l'algorithme SL-Resolution.

 

Les algorithmes énumératif

Ces algorithmes consistent en une exploration systématique de l'ensemble des interprétations afin de déterminer si l’une d'entre elles est un modèle. Cette procédure peut aisément être assimilée à une forme de résolution que l'on nomme résolution dirigée.

On pourra notamment citer la célèbre procédure de Davis et Putnam.

 

La recherche locale

Ces méthodes commencent à donner des valeurs à chaque variables puis vont en modifier certaines itérativement de façon à réduire le nombre de clauses non satisfaites.

On pourra notamment citer le célèbre recuit-simulé.

 

L'approche programmation par contrainte (PPC)

Cette méthode consiste à programmer avec des relations appelées ``contraintes''. Un problème comporte un certain nombre de variables, chacune ayant un domaine, et un certain nombre de contraintes. Trouver une solution à un problème de PPC consiste à décrire l'ensemble des affectations autorisées de chaque variable, de telle sorte que la totalité des contraintes soient satisfaites.

On pourra notamment citer le célèbre algorithme ``Branch And Bound''.