Sudoku Solver Document

About

This page is the document of this web services uses a fast SAT solver to solve Sudoku.
The solver can only solve Sudoku in 9x9 format.

Introduction

This web services uses a fast SAT solver to solve Sudoku.
The solution flow is shown in the figure below.


sudoku_solv

There are three steps before a Sudoku Solver can give a Sudoku answer.

  1. Encoding is the conversion of Sudoku rules and problem information to CNF(Conjunctive normal form).
  2. Solving is to solve the answer of CNF by SAT solver.
  3. Decoding is the process of turning the SAT solver's answer back into a solution to the problem.

Detailed explanation

Please refer to Qiita and GitHub as well.
I have prepared slides for you to see. ( I'm sorry, only Japanese. )

Solving Sudoku by SAT Solver from okmt

Future Work

I plan to to Support Sudoku other than 9x9 format and to make a smartphone app that solves Sudoku.

Link