Utilisation de techniques polynomiales pour la résolution pratique d'instances de SAT
Institution:
ArtoisDisciplines:
Directors:
Abstract EN:
In this Phd-thesis, we focuses on the practical resolution of instances of the SATisfiability problem. We mainly present two works : -the hybridation of complete and uncomplete methods for reduce SAT. The local search is used to guide DPLL-like algorithms to solve efficiently some SAT instances; -some mechanism of clause elimination or clause production thanks to unit propagation are proposed and new polynomial classes for SAT are presented.
Abstract FR:
Dans cette thèse, nous abordons la résolution pratique d'instances du problème de la SATisfiabilité d'une formule booléenne mise sous forme normale conjonctive (SAT) via deux thèmes principaux : -l'hybridation des méthodes de résolution pour SAT. La recherche locale est ici utilisée pour guider des algorithmes de type DPLL afin de résoudre des instances de SAT; -l'utilisation de la déduction restreinte à la propagation unitaire pour produire ou supprimer divers types de clauses dans une formule SAT : un ensemble de prétraitements est proposé et expérimenté. Nous proposons également un ensemble de classes polynomiales utilisant la propagation unitaire comme mécanisme de détection.