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.
This web services uses a fast SAT solver to solve Sudoku.
The solution flow is shown in the figure below.
There are three steps before a Sudoku Solver can give a Sudoku answer.
- Encoding is the conversion of Sudoku rules and problem information to CNF(Conjunctive normal form).
- Solving is to solve the answer of CNF by SAT solver.
- Decoding is the process of turning the SAT solver's answer back into a solution to the problem.
I plan to to Support Sudoku other than 9x9 format and to make a smartphone app that solves Sudoku.