Project SAT-Solving + CSP

• Gute Programmierkenntnisse
• Interesse an Algorithmen für NP-harte Probleme
• Vordiplom

• Implementierung von SAT-Algorithmen oder CSP-Algorithmen
• Erstellung von effizienten Datenstrukturen
• Experimenteller Vergleich der eigenen Implementierung mit bestehenden Solvern auf einem der TOP500 Supercomputer (bwGrid)
• kurze Dokumentation der Herangehensweise und der Ergebnisse in einem Praktikumsbericht.

Die Themen sollen - je nach Umfang - alleine oder in Gruppen bis drei Studenten bearbeitet werden. Zu den von uns vorbereiteten Themen können Sie im Einzelfall selber vorgeschlagene Themen bearbeiten, wenn diese von uns für interessant und umfangreich genug bewertet werden.

Folgende Themen liegen schon vor:

1. Vollständiger SAT-Solver (DPLL like)
2. Stochastischer SAT-Solver, der die Suche nur auf bestimmten Variablen durchführt
3. Änderung eines bestehenden SAT-Solvers (MiniSAT) für bestimmte Aufgaben
4. Implementierung eines Branch and Bound Algorithmus für das Low Autocorrelation binary sequence Problem

Details zu den Themen:

1. Es soll ein SAT-Solver implementiert werde oder ein bestehender so abgeändert werden, dass es möglich ist, um eine Belegung im Hammingabstand d herum alle Lösungen zu finden. 
2. Um stochastische SAT-Solver auf industrielle Probleme anzuwenden, sollte der Solver die Suche nur auf bestimmten Variablen (z.B:  Eingangsvariablen von digitalen Schaltungen) durchführen und die restlichen Variablen (die nur Bedingungen darstellen) ableiten können. Dabei muss der stochastische Solver in der Lage sein, diese Variablen zu identifizieren.
3. MiniSAT gilt als einer der am einfachsten zu verstehenden DPLL Solver. Dieser soll nun so umprogrammiert werden, dass die Aufgaben aus 1 und 2 mit ihm gelöst werden können.
4. Für das Low Autocorrelation Binary Sequence Problem soll ein effizienter Branch and Bound Algorithmus implementiert werden. Der Algorithmus soll in der Lage sein, auf einem Supercomputer zu laufen, sprich das Problem zu parallelisieren. Es wird die Möglichkeit angeboten, auf einem Grid mit über 200 CPUs dieses Program zu testen.

SAT Live! - Meldungen rundum das SAT- Problem

SAT for JAVA - SAT Bibliothek für Java

SAT Library - Solver und Benchamrks rundum SAT

SAT Competition - Wettbewerbe der SAT-Solver

SAT in Ulm - lokale Seite der Mitarbeiter die sich mit dem SAT-Problem beschäftigen

CSP Library - Solver und Benchmarks rundum das CSP - Problem

 

1. Stochastic Local Search Foundations and Applications - Hoos, Holger H.; Stützle, Thomas
2. Handbook of Satisfiability - Biere, A.; Heule, M.; Van Maaren, H.; Walsh, T.;

Die Bücher stehen in der Abteilung zur Verfügung.