In diesem Kurs lernen Sie, wie Sie die Werkzeuge der Erfüllbarkeit (SAT/SMT) anwenden, um eine Vielzahl von Problemen zu lösen. Es werden einige grundlegende Beispiele gegeben, um einen Eindruck von den Anwendungen zu bekommen: das Einpassen von Rechtecken, die für den Druck von Postern verwendet werden sollen, Terminplanungsprobleme, das Lösen von Rätseln und die Korrektheit von Programmen. Außerdem wird die zugrundeliegende Theorie vorgestellt: die Auflösung als grundlegender Ansatz für die propositionale Erfüllbarkeit, das CDCL-Framework zur Skalierung für große Formeln und die Simplex-Methode zur Behandlung linearer Ungleichungen. Der leichtgewichtige Ansatz, um den Kurs Automated Reasoning: satisfiability zu verfolgen, besteht darin, sich nur die Vorlesungen anzusehen und die entsprechenden Quizfragen zu beantworten. Um ein Gefühl für das Thema zu bekommen, mag das gut funktionieren. Der weitaus interessantere Ansatz besteht jedoch darin, SAT/SMT selbst auf verschiedene Probleme anzuwenden, zum Beispiel auf die in der Ehrenaufgabe vorgestellten Probleme.