Home | Impressum | Datenschutz | Sitemap | KIT

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:

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.

Beispiele