SAT-Solving (SudokuSAT)

From International Center for Computational Logic

SAT-Solving (SudokuSAT)

Course with SWS 2/2/0 (lecture/exercise/practical) in SS 2019




  • 2/2/0


Examination method

  • Oral exam


  • 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: