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:

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
  ####
###$ ####
#       #
# #  #  #
#*.  #@ #
#########

Bernhard Beckert