Semantisches Browsen

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
SudokuSAT(WS2018)
Beschreibung <font color="red"> <center> D
<font color="red"> <center> Der Upload startet via Easychair.</center> </font> Here's a preliminary result of the benchmark. Currently the leading solver is <code>#1 - wirkungsfunktional</code>. [[Datei:Benchmark_preview.png|600px]] * Ihr könnt Eure Einreichungen jetzt via Easychair * [https://iccl.inf.tu-dresden.de/w/images/0/07/Verify-sudoku.zip <font color="red">hier</font>] 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 [https://easychair.org/ <font color="red">easychair</font>]. * Für die Registierung, sollt Ihr unter [https://easychair.org/conferences/?conf=sudokusatdd2018<font color="red">SudokuSAT-DD 2018</font>] ** 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 ** [http://tools.computational-logic.org/content/riss.php <font color="red">SAT Solver Riss</font>] , hier [http://tools.computational-logic.org/content/riss/riss_505.zip <font color="red">runteladen</font>] ** unzip ** geht zu /riss_505/bin ** ausführen mit ./riss yourSudokuPuzzleInCNF.cnf * [http://www.labri.fr/perso/lsimon/glucose/#glucose-3.0 <font color="red">SAT Solver Glucose</font>] (Informationen wie es verwendet werden soll, steht unten auf der Seite) * [https://pdfs.semanticscholar.org/535d/06391275618a7b913d1c98a1353286db8d74.pdf <font color="red">hier</font>] 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 * [https://iccl.inf.tu-dresden.de/w/images/a/a7/Sudoku-beispiele.zip <font color="red">Sudokus mit Beispiel fuer Input und Output</font>] ** 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)
il an Johannes, Ort: APB2019 oder KRR Lab)  +
Examination type Klausur  +
Forschungsgruppe Wissensverarbeitung +
Lecturer Steffen Hölldobler +
Modul INF-B-270 + , INF-B-275 + , INF-LE-EUI + , IST-05-PF-HS +
SWSExercise 2  +
SWSLecture 4  +
SWSPractical 0  +
Term WS  +
Title SudokuSAT  +
Tutor Emmanuelle Dietz + , Johannes Fichte + , Marcos Cramer +
Year 2018  +
Hat Abfrage
Dieses Attribut ist ein Spezialattribut in diesem Wiki.
SudokuSAT(WS2018) + , SudokuSAT(WS2018) + , SudokuSAT(WS2018) +
Kategorien Vorlesung
Zuletzt geändert
Dieses Attribut ist ein Spezialattribut in diesem Wiki.
17 Januar 2019 14:17:59  +
verstecke Attribute die hierhin verlinken 
  Keine Attribute verlinken auf diese Seite.
 

 

Bitte den Namen einer Seite angeben, um mit dem Browsen zu beginnen.