Forschungslinie
Forschungslinie
Course with SWS 0/0/0 (lecture/exercise/practical) in SS 2015
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
Calendar
