Forschungslinie

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Forschungslinie

Lehrveranstaltung mit SWS 0/0/0 (Vorlesung/Übung/Praktikum) in SS 2015

Dozent

Umfang (SWS)

  • 0/0/0

Module

Leistungskontrolle

  • Hausarbeit

Diese Vorlesung im Rahmen der Forschungslinien-Vorlesung stellt kurz die Forschung um das Erfüllbarkeitsproblem dar. Weitere Details, auch zu dem damit verbundenen Wettbewerb finden Sie zeitnah auf dieser Webseite.

Wettbewerb
Es soll ein Löser entwickelt werden, der einen Graphen im DIMACS-Graph-Format einlesen kann, und für diesen Graph einen Hamiltonian-Cycle ausgibt, oder ausgibt, dass es keine Lösung gibt. Im Wettbewerb werden mehrere Graphen gelöst. Der Löser, welcher die meisten Graphen in einem gegebenen Timeout (ca. 10 Minuten) erfolgreich lösen kann, gewinnt. Löser, die eine falsche Lösung ausgeben, werden disqualifiziert. Beispielgraphen gibt es hier: http://mat.gsia.cmu.edu/COLOR/instances.html

Abgabetermin
Die finale Version des Werkzeugs muss am Freitag, 3.7., bis 24:00 eingereicht worden sein.

Wettbewerbsumgebung
Unter dem Reiter Termine und Unterlagen wurden Datein für die Wettbewerbungsumgebung und ein Generator für Graphen hinterlegt. Die genutzte Umgebung für den Wettbewerb wird dazu sehr ähnlich sein. Die neuste Version wurde am 30.6. zur Verfügung gestellt.

Format und andere Details

  • das Format für die Lösung ist (da gibt es ein Checker-Werzeug in der Umgebung geben, was nur dieses Format richtig erkennt, und eure Lösungen entsprechend bewertet):
    • kein Cycle:
      "s UNSATISFABLE"
      auf stdout, exitcode 20
    • ein Cycle mit dem Pfad 5->3->4->1->2->5
      "s SATISFIABLE"
      "v 5 3 4 1 2"
      auf stdout, exitcode 10
  • Die Graphen sind eigentlich gerichtet, der Generator liefert für kleine Graphen meist ungerichtete Graphen, da beide Kanten da sind. Für größere Graphen ist das nicht garantiert.
  • Der Generator ordnet die Kanten, darauf kann man sich aber nicht verlassen, falls ich Graphen von außen mit zulasse.
  • Der SAT Solver darf mehrfach aufgerufen werden. Dann interessiert uns was ihr damit genau tut.

Registrierung

Um an dem Wettbewerb teilnehmen zu können, müssen sich die Team von maximal drei Studenten mit einem Teamnamen, sowie der Namen der Studenten und der Matrikelnummer per Email bis zwei Wochen vor dem Wettbewerb bei Norbert Manthey (Vorname.Nachname at tu-dresden.de) registrieren. Eine Vorabversion des Tools muss bis eine Woche vor dem Wettbewerb eingereicht werden, damit sie auf ihre Lauffähigkeit getestet werden kann (der Wettbewerb wird auf einem Linux System ausgetragen). Der Wettbewerb findet nur statt, wenn sich mindestens drei Teams angemeldet haben.

Veranstaltungskalender abonnieren (icalendar)

Vorlesung Vorstellung der SAT Forschung DS5, 13. April 2015 in APB E023 Download
Vorlesung Auswertung des Wettbewerbes DS5, 6. Juli 2015 in APB E023 Download
Vorlesung Graphen des Wettbewerbs DS5, 6. Juli 2015 in APB E023 Download


Kalender