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

Infrastruktur

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
  BBa0h0aBbBa0BcBaBjBb21cBBb
10:b10cB1bBj3a2c1Ba2bBa1hBa22b
  BBa0h0aBbBa0BcBaBjBb21cB0b

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:

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). Auch für Programme, die nicht völlig korrekte Ergebnisse liefern, werden Punkte anteilig vergeben.


Bernhard Beckert