Materialien
Vorlesungsmaterial
Heuristiken zur Lösung von SAT- und QSAT-Problemen - Wintersemester 04/05
Übersicht
| Beschreibung |
Zahlreiche Probleme aus verschiedenen Teilgebieten der Informatik lassen sich reduzieren auf die Lösung sogenannter SAT- bzw. QSAT-Probleme. SAT-Instanzen sind Formeln in konjunktiver Normalform, deren Erfüllbarkeit (Satisfiability) berechnet werden soll, QSAT-Instanzen enthalten darüber hinaus noch Quantifizierungen von Variablen (Existenz- oder Allquantifizierungen). Anwendungen finden sich beispielsweise im automatisierten Schaltungsentwurf, u.a. bei Verifikation ("Berechnen zwei Schaltungen die gleiche Funktion?") , Fertigungstest ("Ist das Fehlverhalten eines bestimmten Gatters an den Ausgängen beobachtbar?") oder Routing ("Lässt sich eine Schaltung gemäß einer vorgegebenen Netzliste innerhalb eines vorgegebenen Gebietes verdrahten?"). SAT- und QSAT-Probleme spielen aber auch eine wichtige Rolle in der künstlichen Intelligenz. Während schon lange bekannt ist, dass SAT und QSAT schwierige Probleme sind (SAT ist NP-vollständig, QSAT PSPACE-vollständig), gab es trotzdem in den vergangenen Jahren eine enorme Entwicklung beim Entwurf von Algorithmen zur Lösung von SAT- und QSAT-Instanzen. Hierbei konnte beobachtet werden, dass Probleminstanzen, die in praktischen Beispielen auftreten, (unter Ausnutzung der Problemstruktur) häufig effizient gelöst werden können. Das Seminar führt durch die Vorstellung von Originalarbeiten an den aktuellen Stand der Forschung auf diesem Gebiet heran. |
| Kommentar |
Block-Seminar |