Sat Solving

Inhalt

Das aussagenlogische Erfüllbarkeitsproblem SAT ist das prominenteste NP-vollständige Problem. Aus theoretischer Sicht ist es das erste NP-vollständige Problem, was heißt, dass es „wahrscheinlich“ keine effizienten (im Sinne von Polynomialzeit) Algorithmen dafür gibt. Aus praktischer Sicht ist es interessant, weil es in den letzten zwei Jahrzehnten trotzdem sehr große Fortschritte bei der Implementierung von SAT solvern gab (also Programmen, die SAT lösen können). Mit aktuellen SAT solvern lassen sich oft Instanzen mit mehr als 100000 Variablen und Klauseln in realistischer Zeit lösen. Mit Hilfe von SAT solvern konnten zudem teilweise lange offene Probleme aus der Mathematik gelöst werden. Im Proseminar werden wir diese Themen näher betrachten. 

Organisation

Das Proseminar wird semesterbegleitend stattfinden. Das erste Treffen findet in der ersten Vorlesungswoche statt.