| note
| - Le problème SAT est un cas particulier du problème de satisfaction de contraintes où les variables prennent la valeur booléenne 0 ou 1. Le problème de satisfaction de contrainte lui-même joue un rôle central dans l'intelligence artificielle (IA). L'étude du problème SAT a une forte utilité pratique car il est à la base de très nombreux problèmes d'IA, notamment la déduction automatique, le contrôle de circuits VLSI, la programmation logique, l'apprentissage, l'ordonnancement, etc. en 1962, Davis, Logemann et Loveland ont présenté leur algorithme, appelé ensuite procédure DPL, pour résoudre le problème SAT. Selon cette procédure, des systèmes complets ont été crées, par exemple, Grasp, Posit, Relsat(4), Satz, etc. notre travail se situe précisément au sein du domaine des études empiriques pour la résolution du problème SAT en utilisant les systèmes complets. Tout d'abord, nous réalisons une étude empirique pour trouver quelques propriétés intéressantes correspondant à la difficulté de la résolution des problèmes 3-SAT aléatoires, en utilisant les systèmes différents. Puis, nous contribuons à l'amélioration du système Satz, en mettant en œuvre une série d'expérimentations utilisant heuristiques UP différentes. Nous utilisons ensuite Satz pour analyser les arbres produits par ce système, pour réaliser la comparaison avec les systèmes les plus performants de la littérature et également pour créer quelques extensions. Enfin, nous essayons d'expliquer la performance de Satz par l'hypothèse de contrainte. Nos expériences dans ce travail renforcent la conviction que l'heuristique UP est puissante pour les problèmes SAT aléatoires, et elle l'est aussi pour les problèmes SAT structures. Nous pensons également que la stratégie essentielle, pour implanter la procédure DPL dans un système, est d'essayer d'atteindre une contradiction aussi vite que possible ; d'autre part, selon nous, les heuristiques sont probablement la méthode la plus efficace pour mettre en œuvre de telles stratégies. Toutefois, si les heuristiques venaient à ne pas bien fonctionner, il faudrait recourir à d'autres méthodes. Par exemple, pour les problèmes ou la plupart des variables sont symétriques, il pourrait être judicieux d'essayer des méthodes telles que l'apprentissage ou la détection de symétrie. Satz pourrait être amélioré dans ce sens. Il n'existe a ce jour aucun système capable de résoudre tous les problèmes NP-complets et en particulier les problèmes SAT. Les systèmes qui existent actuellement ne résolvent que certaines classes du problème SAT.
|
![[RDF Data]](/fct/images/sw-rdf-blue.png)
