Résolution propositionnelle et solveurs SAT

Cette séance de cours couvre la transformation des formules en forme normale conjonctive, la complexité de ces transformations et l'efficacité des algorithmes de vérification de la satisfaction. Il traite de l'équivalence, de l'équisatisfaction, de la transformation de Tseytin et de l'algorithme DPLL. La séance de cours explore également les structures de données dans les solveurs SAT, la propagation des unités, la subsomption et l'apprentissage des clauses axé sur les conflits.