SAT-Solving (SudokuSAT)

From International Center for Computational Logic

SAT-Solving (SudokuSAT)

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

Lecturer

Tutor

SWS

  • 2/2/0

Modules

Examination method

  • Oral exam

Submission

  • Deadline: tba

Installation

  • https://github.com/rkkautsar/sudokusat-example
    • Install the sudoku experiment including repobench as described in the README.md
  • Your solver goes under "my_solver/my_solver.sh" (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 my_solver.sh)
  • 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: https://easychair.org/conferences/?conf=sudokusatdd2019