Séminaire de Sami Cherif - Université d'Aix Marseille
Raisonnement et inférence pour la satisfiabilité (maximum)
20 mars 2023 - 14:00Au cœur de l’informatique et de l’intelligence artificielle, la logique est souvent utilisée comme un langage pour modéliser et résoudre des problèmes complexes issus du milieu académique ou d’applications industrielles. Un formalisme bien connu dans ce contexte est le problème de Satisfiabilité (SAT) qui vérifie simplement si une formule propositionnelle donnée sous la forme d’un ensemble de contraintes, appelées clauses, peut être satisfaite. Une extension naturelle de SAT en problème d’optimisation est la Satisfiabilité Maximum (Max-SAT), qui consiste à déterminer le nombre maximal de contraintes clausales pouvant être satisfaites dans la formule. Dans ce séminaire, je présenterai certaines thématiques abordées durant ma thèse. Tout d’abord, je présenterai des travaux dédiés à SAT et en particulier à l'intégration de techniques issues de l'apprentissage par renforcement dans les solveurs modernes pour ce problème. Dans ces travaux, on montre qu'une sélection adaptative d’heuristiques de branchement grace à un formalisme bandit manchot permet d’améliorer l’efficacité des solveurs modernes. Ensuite, je présentrai des travaux autour des systèmes de preuve pour Max-SAT. L'objectif majeur de ces travaux est de combler le fossé théorique entre l’inférence SAT et Max-SAT, permettant ainsi d'introduire un générateur de preuves indépendant pour Max-SAT.