tdoku

For a casual effort this solver is quite fast. On most datasets it's significantly faster than a C++ port of the Norvig solver and it's often in the same league as well-tuned DLX solvers (though still not in the major league). Relative to DLX it's faster on the easiest puzzles and slower on hard ones, though its performance degrades significantly in two specific still-easy cases: (1) 17-clue puzzles since these punish solvers that don't propagate hidden singles, (2) 0-solution puzzles since the solver doesn't check for consistency during initialization (something the author acknowledges in a comment). For context see these benchmarks from a modern laptop (https://github.com/t-dillon/tdoku/blob/master/benchmarks/res...) and compare lhl_sudoku to the other simple solvers tdev_basic_heuristic, zerodoku, fast_solv_9r2, kudoku, and norvig. For

Sudoku may be a poor example for illustrating some of the overarching points of this series of blog posts, which I take to be that modern SAT solvers are, as someone described them in a previous thread, "little diamonds of engineering", that they embody decades of research, that you can exploit their power cheaply and easily, and that it might take significant effort to beat them if you have a non-trivial problem. Since specialized solvers do thrash SAT-based solvers for conventional Sudoku, the author focuses the example less on absolute performance and more on simplicity, rapid prototyping, and comparison to casual non-SAT implementations. But conventional Sudoku is a small problem, and in most cases the SAT-based solver makes so few decisions that it doesn't benefit much from CDCL. Consider here[1] the comparison to JCZSolve(ZSolver) t

Bear in mind that JSolve was 5x faster than the fastest DLX solver in the attractivechaos 2011 benchmarks, and today there are several solvers that are 2x faster than JSolve (https://github.com/t-dillon/tdoku/tree/master/benchmarks). If the difference is really an order of magnitude, that's pretty non-competitive. I certainly don't mean do disparage DLX. It's a powerful and general algorithm. But if you need a fast Sudoku solver (for puzzle mining or studying Sudoku research questions) then it's not the tool I'd reach for. The backtracking solvers just get a lot of mileage out of tuning their representation to play nicely with hardware. They also blow general purpose CDCL SAT solvers out of the water, at least for 9x9 Sudoku.

There is a collection of benchmarks of the fastest sudoku solvers here: https://github.com/t-dillon/tdoku/tree/master/benchmarks How fast they are depends on the difficulty of the sudoku and on your machine, but it's typically a few thousand/s on the hardest known and several 100k/s to a million/s on very easy.