Introduction aux différents aspects du raisonnement automatique, dont l’objectif est de permettre d’obtenir des solutions à tout type de problèmes uniquement à partir de leurs descriptions et grâce à des solveurs générant une preuve du résultat inspiré du raisonnement humain. Cette UE aborde les formalismes les plus simples, les problèmes SAT et CSP binaires, qui correspondent à des problèmes de décision, et étudie la façon de modéliser un problème dans ces formalismes, les méthodes de résolution arborescente (avec filtrages, heuristique de choix de variable, de valeur), et des solveurs existants (Minisat, Choco).