Eli Bendersky's website Once I had a task at work of doing some coding for a SAT solver.
To learn more about SAT solvers, I read some papers and tutorials about DPLL - an algorithm to solve SAT which is used as the basis for many modern solvers. To consolidate my understanding of the algorithm, I wrote a short document (dpll.pdf in the package) and coded the algorithm in Perl. The implementation is very simplistic because no heuristic is used. Real SAT solvers are all about complex, sophisticated heuristics.
When Sudoku became popular, I solved a few and quickly reached a conclusion that I don't find these puzzles interesting. The solution process just felt too mechanic, and reminded me of manually solving a boolean formula for satisfiability (SAT) - the same approach of applying clearly defined inference rules over and over again until a solution is reached. So I searched the net a little (the Google search "sudoku sat" should get you started) and came upon a few interesting websites and articles that discuss representing Sudoku as a SAT problem. Since I already had a (very) modest SAT solver of my own, I decided to implement the other half of the problem and make it all work together to actually solve Sudokus.
At the same time I started being interested in Ruby, so I wanted to combine the interests and code the solver in that language. I've rewritten my Perl SAT solver in Ruby and added a Sudoku solver, which is capable of solving even the hardest Sudokus without any guessing, as far as I know of.
Download the package from here.