SudokuSAT
Aus International Center for Computational Logic
SudokuSAT
Lehrveranstaltung mit SWS 4/2/0 (Vorlesung/Übung/Praktikum) in WS 2018
Dozent
- Steffen Hölldobler
Tutor
Umfang (SWS)
- 4/2/0
Module
Leistungskontrolle
- Klausur
Here's a preliminary result of the benchmark.
Currently the leading solver is #1 - wirkungsfunktional.
- 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
- Windows/OSX Nutzer, wenn möglich vorher folgende Programme installieren
- Virtual Box: https://www.virtualbox.org/wiki/Downloads
- Vagrant: https://www.vagrantup.com/
- Ubuntu 16.04 Box herunterladen und einmal hochfahren:
- Kommandozeile öffnen (Windows cmd; OSX: Terminal (EN), Kommandozeile (DE) unter Utilities)
- folgende Kommandos ausführen
- vagrant init ubuntu/xenial64 #installiert die Box lokal / Netzwerkverbindung erforderlich
- vagrant up #Fährt das Gastbetriebssystem hoch
- vagrant ssh #Verbindet sich zum Gastbetriebssystem
- exit #Verbindung schliessen
- vagrant suspend #Gastbetriebssystem anhalten und letzten Zustand speichern
- Details
- Tutorial: https://www.vagrantup.com/intro/getting-started/
- Ubuntu Box: https://app.vagrantup.com/ubuntu/boxes/xenial64 (New)
- Ubuntu Nutzer
- SAT Solver Riss , hier runteladen
- unzip
- geht zu /riss_505/bin
- ausführen mit ./riss yourSudokuPuzzleInCNF.cnf
- SAT Solver Glucose (Informationen wie es verwendet werden soll, steht unten auf der Seite)
- 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)
