Tjark Weber. In Geoff Sutcliffe and Andrei Voronkov, editors, LPAR-12, The 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Short Paper Proceedings, pages 11-15, December 2005.
This paper presents a SAT-based Sudoku solver. A Sudoku is translated into a propositional formula that is satisfiable if and only if the Sudoku has a solution. A standard SAT solver can then be applied, and a solution for the Sudoku can be read off from the satisfying assignment returned by the SAT solver. No coding was necessary to implement this solver: The translation into propositional logic is provided by a framework for finite model generation available in the Isabelle/HOL theorem prover. Only the constraints on a Sudoku solution had to be specified in the prover's logic.
@inproceedings{weber05satbased,
author = {Tjark Weber},
title = {A {SAT}-based {Sudoku} Solver},
editor = {Geoff Sutcliffe and Andrei Voronkov},
booktitle = {LPAR-12, The 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Short Paper Proceedings},
pages = {11--15},
month = dec,
year = {2005}
}