SAT-Solving (SudokuSAT)

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

SAT-Solving (SudokuSAT)

Lehrveranstaltung mit SWS 2/2/0 (Vorlesung/Übung/Praktikum) in SS 2019


  • Steffen Hölldobler


Umfang (SWS)

  • 2/2/0



  • Mündliche Prüfung


  • Deadline: tba


    • Install the sudoku experiment including repobench as described in the
  • Your solver goes under "my_solver/" (or you can just use the bash file to wrap your solver)
  • You can find examples under "examples/bsp-sudoku-input.txt" etc.
  • We placed testing instances for you under "sudokusat-example/instances/"
  • For the solver we assume that you allow to use multiple SAT solvers (we provide the name of the solver as first parameter to the call (see
  • We will test the solvers clasp, glucose, and riss
  • To install a SAT solver we suggest you take clasp
    • It is available as binary for all common platforms.
    • Therefore, visit the clingo github repository and download clingo-5.3.0-linux-x86_64.tar.gz (for linux) etc.
    • Unpack the file into some directory (X)
    • Copy the file clasp from X into the folder ./sudokusat-example/env/bin
  • Register your Group on Easychair: