Formale Systeme
Wahlpflichtvorlesung/Stammmodul im Wintersemester 2009/2010
Prof. Dr. Bernhard Beckert, Dr. Vladimir Klebanov
Details zur Auswertung der Praxisaufgabe 1 "SAT-o-ban"
Alle Punktzahlen sind vorläufig. Möglich sind noch Punktekorrekturen wegen Gruppenarbeit.
Es gab 119 Einreichungen, davon produzierten 101 eine (mehr oder weniger, s.u.) korrekte Lösung.
Nicht unerhebliche Anzahl der Einreichungen hatten folgende Probleme:
- Syntaxfehler beim Kompilieren
- Exceptions beim Ausführen aufgrund von falschen Dateinamen
- Gesetzter DEBUG Flag
- Falsch formatierte Ausgabe
Diese wurde korrigiert und nicht mit Punkteabzug bestraft.
Nicht unerhebliche Anzahl der Einreichungen hatten DEPTH trotz Hinweis nicht als Zahl der Zustände, soncern als Zahl der Züge interpretiert. Dies führte ebenfalls nicht zur Abwertung.
Performanz wurde ebenfalls nicht gewertet. Die schnellste (korrekte) Einreichung brauchte für die Testeingabe ca. 1,8 Sekunden, die langsamste ca. 87 Sekunden. Schnitt lag bei 10,5 Sekunden (alle Werte ermittelt mit minisat).
Testeingabe und Referenzausgabe
ullddlddrruluuurrdluldddullddrruuld UNSAT UNSAT UNSAT ;;DEPTH: 36 # ##### # # ###$$@# # ### # # # . . # ####### ;;DEPTH: 35 # ##### # # ###$$@# # ### # # # . . # ####### ;;DEPTH: 34 # ##### # # ###$$@# # ### # # # . . # ####### ;;TITLE: Test for container framing ;;DEPTH: 8 #### ###$ #### # # # # # # #*. #@ # #########