## 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.

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.

### Detailed explanation

Please refer to Qiita and GitHub as well.

I have prepared slides for you to see. ( I'm sorry, only Japanese. )

## Future Work

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

## Link