Reconnaissance et exploitation de propriétés structurelles pour la résolution du problème SAT
Institution:
ArtoisDisciplines:
Directors:
Abstract EN:
The satisfiability problem of propositional logic (SAT) captures the essence of many difficult problems in disciplines such as artificial intelligence, computer science, electrical engineering and operations research. It concers the problem of deciding whether or not a logical formula contains a contradiction. In general no efficeint algorithms are available to solve it but some specific classes of SAT allow efficient algorithms. These last years, new algorithms were developed that in practice seem to suffer less from the combinatorial explosion. First, we propose a new pre-processing step in the resolution of SAT instances that recovers and exploit some structural knowledge that is hidden in the formula. New simplifications are also proposed. All these extractions and simplifications techniques allowed us to implement a new SAT solver that proves to be the most efficient current one with respect to several important classes of instances. Then, a branching criterion initialy introduced by Purdom is revisited and extended. It is shown very efficient from a practical point of view in that it allows search trees in SAT solving to be pruned in a significant way. New method combining resolution and enumeration is finally proposed to produce new informations.
Abstract FR:
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. Il n'existe pas à l'heure actuelle d'algorithmes permettant de le résoudre efficacement. Néanmoins, certaines classes (traitables) du problème SAT admettent des algorithmes efficaces. Ces dernières années, de nouvelles méthodes de résolution sont apparues et semblent moins souffrir de l'explosion combinatoire en pratique sur de nombreux problèmes. Dans une première partie, nous énonçons quelques définitions au sujet de la logique propositionnelle, fixons les notations et présentons le problème SAT. Nous présentons en seconde partie une première contribution. Celle-ci porte sur l'extraction et l'utilisation d'informations structurelles exprimées sous la forme de fonctions booléennes à partir d'une formule CNF. Ces travaux ont abouti au développement d' un nouveau solveur : LSAT. En troisième partie, nous présentons une nouvelle forme d'apprentissage (principe de recherche complémentaire proposé par Purdom) et proposons une méthode combinant résolution et énumération dans le but de produire de nouvelles informations. Ces approches constituent notre contribution aux techniques prospectives et rétrospectives.