SudokuSAT

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

SudokuSAT

Lehrveranstaltung mit SWS 4/2/0 (Vorlesung/Übung/Praktikum) in WS 2018

Dozent

Tutor

Umfang (SWS)

  • 4/2/0

Module

Leistungskontrolle

  • Klausur

Hier findet Ihr alle Informationen zu dem Sudoku SAT Wettbewerb

  • hier könnt Ihr Eure Sudokus validieren
  • Der Wettbewerb wird im Januar 2019 stattfinden

Installation

  • hier sind die Constraints in cnf für das Sudoku Problem wie in den Übungen besprochen. Bei dem letztem Constraint des extended encoding (Seite 5) ist ein Fehler: Das Oder am Anfang muss durch ein Und ersetzt werden, und die beiden letzten Unds müssen durch Oders ersetzt werden
  • Sudokus mit Beispiel fuer Input und Output
    • bsp-sudoku-input.txt ist die Form des Inputs
    • bsp-sudoku-for-SAT.cnf ist eine moegliche Form wie das bsp-sudoku-input.txt in cnf kodiert werden kann
    • bsp-sudoku-SAT-sol.txt ist der Output des SAT solvers fuer die oben gegebene Kodierung
    • bsp-sudoku-output.txt ist der lesbare und gewünschte Output
    • der sudokus Ordner enthält Sudokus von verschiedenen Grössen zum Testen
  • Konsultation bei Installationsproblemen
    • 22.11. 1.DS (Reguläre Übung bei Johannes; regelmäßige Studenten der Übungsgruppe haben Vorrang)
    • 28.11. 14 Uhr (bitte vorher kurze Anmeldung per Mail an Johannes, Ort: APB2019 oder KRR Lab)