Résumé : Le problème NP-complet classique de la satisfiabilité d'une formule Booléenne mise sous forme normale conjonctive a connu un intérêt croissant non seulement dans la communauté d'informatique théorique, mais aussi dans des domaines d'applications divers ou une solution pratique à ce problème permet des avancées significatives. Depuis les premiers développements de la procédure de base proposée par Davis, Putnam, Logemann et Loveland (DPLL), il y a plus d'une quarantaine d'années, ce domaine a connu un effort de recherche croissant ayant abouti aux solveurs SAT modernes d'aujourd'hui, capable de résoudre des instances de plusieurs centaines de milliers et même de millions de variables. Dans cet exposé, nous examinerons les idées principales ayant permis ce passage à l'échelle et nous évoquerons quelques applications de SAT.

 

Bibliographie :

Pr. Said Jabbour a obtenu son doctorat de l'université d'Artois en décembre 2008 après un master en 2004 et un diplôme d'ingénieur de l'ENSEM de Nancy en 2002. Après un post-doc à l'INRIA-Microsoft à Paris en 2009, il est recruté en tant que maître de conférences à l'université d'Artois en 2010. Il obtient son Habilitation à diriger des Recherches en 2018. Ses thématiques de recherche s’inscrivent à la frontière de plusieurs domaines différents incluant l’Intelligence Artificielle (IA), la fouille de données et les systèmes d’information. Elles peuvent être caractérisées par les mots clés suivants : programmation par contraintes, représentation des connaissances, la problématique de raisonnement sur des ontologies conflictuelles (incohérentes et/ou inconsistantes) via l’argumentation déductive, fouille de motifs sous contraintes, clustering, détection de communautés, compression de données et composition de services web.