LMU - Ludwig-Maximilians-Universität München
Theoretische Informatik
Links und
Sprachumschaltung
Bachelor- und Masterarbeiten
Paritätsspiele durch Reduktion auf SAT lösen
Frühere Semester
Verifizierte Standardbibliothek für die funktionale Sprache Agda
Implementierung eines Typsystems für Objektorientierte Programme
Untersuchung der Verwendbarkeit von SAT-Solving zur Schulstundenplanung
Effiziente Termrepräsentationen für Typisierungsalgorithmen
Schüler an der Uni
Fortgeschrittenenpraktikum
Aufgabenstellung:
In einem Paritätsspiel bewegen zwei Spieler (I und II) ein Pebble über einen endlichen, gerichteten Graphen. Jeder Knoten hat eine Priorität (natürliche Zahl). Spieler I gewinnt, falls die kleinste Priorität, die unendlich oft besucht wird, gerade ist. Ansonsten gewinnt Spieler II. Das Problem, ein Paritätsspiel zu lösen (PARITY), besteht darin die Menge aller Knoten zu bestimmen, von denen Spieler I aus eine Gewinnstrategie für das Spiel hat.Dieses sehr konstruiert anmutende Problem hat dennoch hohe praktische Relevanz. PARITY ist äquivalent zum Model Checking Problem für den modalen μ-Kalkül und damit interessant für die Programmverifikation.Auch theoretisch gesehen ist PARITY interessant: Es ist eins der wenigen Problem, die in NP liegen, aber nicht NP-hart sind, und von dem nicht bekannt ist, ob es in P liegt. Letzteres wird jedoch stark vermutet. Alle bisher bekannten Algorithmen haben eine Laufzeit, die exponentiell in der Anzahl der verschiedenen Prioritäten ist.Da PARITY in NP liegt, gibt es eine polynomielle Reduktion auf SAT, das Erfüllbarkeitsproblem für die Aussagenlogik. Obwohl dieses NP-hart ist, sind in den letzten Jahren unheimliche Fortschritte gemacht worde, sogenannte SAT-Solver zu entwickeln, die noch sehr grosse aussagenlogische Formeln effizient auf Erfüllbarkeit testen können.Ziel dieses Fortgeschrittenenpraktikums ist es, die Reduktion von PARITY auf SAT zu implementieren und somit PARITY durch einen SAT-Solver lösen zu lassen. Die Implementierung soll mit bisher bekannten Algorithmen für PARITY, z.B. Jurdzinski und Vöge's Strategieverbesserungs-Verfahren, verglichen werden.Bemerkung: Die Reduktion von PARITY auf SAT eröffnet einen weitere Möglichkeit zu zeigen, dass PARITY in P liegt (falls dies gilt). Dies ist geschehen, sobald es gelingt, die speziellen Formeln, die durch diese Reduktion entstehen, in polynomieller Zeit auf Erfüllbarkeit zu testen. Dies soll allerdings nur motivieren, selbst aber nicht Teil des Fortgeschrittenenpraktikums sein. Literatur/Material/Links:
M. Jurdzinski, J. Vöge, A Discrete Strategy Improvement Algorithm for Solving Parity Games.In Proceedings of 12th Int. Conf. on Computer Aided Verification, CAV 2000, July 2000, Copyright 2000 Springer-Verlag .SATLive, eine Menge zu SAT und SAT-Solvern.M. Lange, Solving Parity Games by a Reduction to SAT, in Arbeit.
Dr. Martin Lange
Funktionsleiste