25.05.2016 · Uwe Schöning · Universität Ulm · Algorithmen für das Erfüllbarkeitsproblem SAT

SchoeningDas SAT-Problem ist das erste, von dem die NP-Vollständigkeit nachgewiesen werden konnte, ebenso von dem eingeschränkten Problem 3SAT. Trotz NP-Vollständiglkeit zeigt sich, dass so genannte SAT-Solver in vielen Fällen Instanzen des SAT-Problem mit Tausenden von Variablen effizient lösen können. Es werden verschiedene Arten von SAT-Algorithmen besprochen, sowohl Backtracking-basierte als auch solche, die mit lokaler Suche arbeiten.