Séminare DKM. SAT : résoudre un problème difficile pour les résoudre tous

Laurent Simon (LABRI)
Thursday, November 28, 2019 - 10:30
Room Markov
Talk abstract: 

Les progrès autour de la résolution pratique du problème SAT, le problème NP-Complet canonique, ont été spectaculaires dans certains domaines applicatifs. Même si des limites fortes existent toujours sur quelques problèmes fortement combinatoires, nous présenterons, dans cet exposé, quelques applications clés qui ont bénéficié de ces progrès.Nous présenterons également comment la logique propositionnelle, au coeur de SAT, permet de modéliser et de résoudre des problèmes de raisonnement bien au delà de ce formalisme initial. Ainsi, l'exposé se conclura par la présentation des progrès récents en compilation de connaissance, formalisme puissant, général et élégant pour le raisonnement.