Sudoku is a very simple and well-known puzzle that has achieved international popularity
in the recent past. This paper addresses the problem of encoding Sudoku puzzles into conjunctive
normal form (CNF), and subsequently solving them using polynomial-time propositional
satisfiability (SAT) inference techniques.

Sudoku isn't the only thing that you can use a SAT solver on ;-) Luckily I wrote a SAT Solver in college which uses a modified DLPP algorithm with back propagation and some heavy preprocessing for initial value selection.