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