SudokuSAT

From International Center for Computational Logic

SudokuSAT

Course with SWS 4/2/0 (lecture/exercise/practical) in WS 2018

Lecturer

Tutor

SWS

  • 4/2/0

Modules

Examination method

  • Written exam



Der Upload startet via Easychair.

Here's a preliminary result of the benchmark.

Currently the leading solver is #1 - wirkungsfunktional.

Benchmark preview.png

  • Ihr könnt Eure Einreichungen jetzt via Easychair
  • hier könnt Ihr Eure Sudokus validieren

Submission

  • Deadline: erste Version 15. Jan. 2019
  • zip file im easychair hochladen
  • Inhalt des zip files: solver; dieser sollte via makefile or cmake gebaut werden können ohne große aufwände
  • falls der upload mit der endung zip nicht klappen sollte bitte in pdf umbennenen ;-)
  • name des solvers/binary/start script (titel im easychair; kein "-" oder leerzeichen im titel
  • Ausführung via Kommandozeile: "sudokusolver sudoku1.txt"
  • Wir geben dann jeweils Rückmeldungen, ob es geklappt hat ...
  • Das Programm soll am Ende ein sudoku erzeugen, aber der call soll austauschbar sein (riss/glucuse).
  • Riss/glucose werden in der Systemumgebung unter den Namen riss und glucose im path zur Verfügung stehen.
  • Wichtig ist, dass wir am Ende mit dem validator auch validieren können inwieweit das sudoku gültig ist, was wir aus dem sat solver raus bekommt. Es muss also ein Sudoku im output format per standard-out (siehe unten) ausgegeben werden.


Registrierung

  • Um Euch für das Wettbewerb zu registrieren, braucht mindestens eine_r aus der teilnehmenden Gruppe einen Account bei easychair.
  • Für die Registierung, sollt Ihr unter SudokuSAT-DD 2018
    • einloggen
    • bei 'new submission' die Namen der Gruppenmitglieder angeben
    • bei 'abstract' den Namen der Gruppe angeben (mit dem Ihr am Wettbewerb teilnehmen wollt)

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)