Formale Systeme
Vorlesung im Wintersemester 2014/2015
Prof. Dr. Bernhard Beckert (BB)
Thorsten Bormer (TB),
Dr. Vladimir Klebanov (VK),
Dr. Mattias Ulbrich (MU)
Praxisaufgabe 1: SAT Solver — "Spotlight"
Das Logik-Puzzle "Spotlight" ist eine NP-vollständige Denksportaufgabe, die wir in dieser Praxisaufgabe mit Hilfe eines aussagenlogischen SAT(isfiability) Solvers lösen wollen.
Für die vollständige Lösung dieser Praxisaufgabe erhalten Sie 20 Bonuspunkte fur die Abschlussklausur.
Auch für Teillösungen, die nicht in allen Fällen korrekte Ergebnisse liefern, werden Punkte anteilig vergeben.
Material
Das Aufgabenblatt enthält alle notwendigen Hinweise zur Bearbeitung der Aufgabe:- Aufgabenblatt
- Rahmenwerk zur Implementierung
- SAT4j sat solver, siehe dazu auch www.sat4j.org
- JavaDoc Dokumentation zum Rahmenwerk
- Schablonendatei für Ihre Lösung
Abgabe
Die Abgabe der Praxisaufgabe erfolgt über das ILIAS-Portal.
Testen Ihrer Lösungen
Wir haben darüber hinaus einen Dienst installiert, der Ihre Lösungen automatisiert übersetzt und mit einigen Beispielproblemen konfrontiert. Sie können das Protokoll dieses Laufes einsehen, sobald dieser erfolgt ist.
Um diesen automatisierten Test nutzen zu können, müssen Sie sich einmalig unter auf dieser Seite mit Ihrer Matrikelnummer registrieren.
