Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation

Formale Systeme

Vorlesung im Wintersemester 2015/2016

Prof. Dr. Bernhard Beckert (BB)
Dr. Thorsten Bormer (TB), Dr. Vladimir Klebanov (VK), Dr. Mattias Ulbrich (MU)

Praxisaufgabe 1: SAT-Solver – "Light Up" lösen

Das Logik-Puzzle "Light Up" ist eine NP-vollständige Denksportaufgabe, die Sie in dieser Praxisaufgabe mit Hilfe eines aussagenlogischen SAT(isfiability) Solvers lösen sollen.

Lernziele:

Sie können eine abstrakte Problemstellung als aussagenlogische

Fragestellung umformulieren und sind in der Lage ein Programm zu entwickeln, das für konkrete Probleminstanzen aussagenlogische Klauselmengen, die eine Lösung beschreiben, erzeugt. Sie kennen das Format DIMACS zur Kodierung aussagenlogischer Probleme und haben können mit dem Werkzeug SAT4J umgehen.

Abgabe Ihrer Lösungen bis spätestens zum 6.1.2016.

Für die vollständige Lösung dieser Praxisaufgabe erhalten Sie 10 Bonuspunkte für die Abschlussklausur (die im Verhältnis 1:10 angerechnet werden). Die Abgabe erfolgt über die Ilias-Plattform. Auch für Teillösungen, die nicht in allen Fällen korrekte Ergebnisse liefern, können Punkte anteilig vergeben werden.

Material zur Aufgabe

Eine ausführliche Beschreibung der Aufgabe finden Sie im Aufgabenblatt.

Weitere Informationen zu Light Up

Animation, die die Regeln von Light Up beschreibt und weitere Infos: Akari tutorial
Eine Javascript-Implementierung von Light Up: Light Up (aus einer Sammlung weiterer interessanter Puzzles)
Weitere Webseite, auf der man Light Up online spielen kann: Light Up

Weitere Informationen zu SAT4J

Zur Lösung der Aufgabe wird das SAT-Rahmenwerk SAT4J verwendet, ein Implementierung einer Lösungsroutine für aussagenlogische Entscheidungsprobleme, die vollständig in Java geschrieben ist. Gegenüber in C oder in anderen nativen Sprachen geschriebenen Solvern ist SAT4J etwas langsamer, dafür vollkommen portabel.

Homepage: www.sat4j.org

Material zur Aufgabe

Offenes Testbett

Sie können hier eine Datei, die die Klasse MyLightUpSolver enthält, hochladen. Wir lassen diese Implementierung dann gegen eine Menge von Testfällen bei uns laufen und Sie erhalten von uns Feedback zu diesen Testfällen per E-Mail.

Die Bearbeitungszeit dieser Aufgabe ist abgelaufen, daher ist die Abgabe geschlossen.

Bei Fragen und Problemen mit dieser Abgabe kontaktieren Sie bitte M. Ulbrich.