Formale Systeme
Wahlpflichtvorlesung im Wintersemester 2008/2009
Prof. Dr. Bernhard Beckert (im WS 08/09 Universität Karlsruhe und Universität Koblenz-Landau), Mattias Ulbrich
Zurück zur Vorlesungswebseite
Praxisaufgabe 1: SAT-Solver - Light Up lösen mit MiniSat
Abgabe bis zum 31.12.2008. Für die vollständige Lösung dieser Praxisaufgabe erhalten Sie 1,5 Bonuspunkte für die Abschlussklausur (bitte beachten Sie die Erläuterung zu Bonuspunkten auf der Webseite zur Vorlesung).
Hier steht eine mögliche Lösung als Java-Implementierung.
Beschreibung der Aufgabe
Eine ausführliche Beschreibung der Aufgabe finden Sie in diesem Dokument: praxis1.pdf
Weitere Informationen zu Light Up und MiniSat
- Flash-Animation, die die Regeln von Light Up beschreibt: Akari tutorial
- Webseite, auf der man Light Up online spielen kann: Light Up
-
Homepage von MiniSat: The MiniSat Page
Von dort können Sie auch die aktuelle Version herunterladen, wenn Sie MiniSat selbst installieren und nicht die auf den Pool-Rechnern der ATIS vorhandene Version verwenden wollen.
Infrastruktur
- Paket mit Java-Klassen, die für die Lösung dieser Praxisaufgabe nützlich sind: lightup.src.zip
- Dokumentation in JavaDoc zu diesen Klassen: Dokumentation
Spielbretter, für die die Lösungen abgegeben werden sollen
| Aufgabe 1 | Aufgabe 2 |
|---|---|
 |
 |
| Zeichenkette für die Aufgabe | Zeichenkette für die Aufgabe |
Kleinere Beispiele
| Beispiel vom Übungsblatt | Alle Wandarten treten auf | Beispiel der Größe 10 | Unerfüllbares Beispiel |
|---|---|---|---|
 |
 |
 |
 |
5:i1g1a1c0B |
7:BBb3aBaBiBBi1a2c0c4aBg |
10:b10cB1bBj3a2c1Ba2bBa1hBa22b |
10:b10cB1bBj3a2c1Ba2bBa1hBa22b |
Abgabe der Lösungen
Die Abgabe der Lösung erfolgt hier: LOGIN (beim ersten Login Registrierung mit der Matrikelnummer). Hochgeladene Lösungen können bis zum 31.12. verbessert werden.
Die Lösung besteht aus:
- Lösungen zu den beiden oben gezeigten Spielbrettern, das heißt die Zeichenketten für die Bretter mit platzierten Lampen,
- dem Quelltext (als ASCII-Text) Ihres Java-Programms.