Writing Sudoku Solvers

After writing a Nonogram solver, I decided to tackle a Sudoku solver to practice Rust. My goal wasn't just to support classic Sudoku rules, but also to handle variants like Thermometer, Arrow, and Cage etc.

1. Brute Force

It is fairly easy to write a brute force or backtracking algorithm. This approach is sufficient for most classic Sudoku puzzles, but it becomes unbearably slow as soon as variant rules are introduced.

I considered this step a warmup—a baseline to improve upon.

2. Constraint Propagation

Here, I tried to introduce "logical thinking" to the algorithm. I used u16 as a bitmask to represent the possible values of a cell. Whenever a cell's state changes (due to guessing, backtracking, or propagation), the algorithm consults all constraints to eliminate impossible candidates.

While Nonogram is technically an NP-Complete problem, in practice, my constraint-propagation solver (without guessing) can solve almost all puzzles found online. I’ve only seen one exception where I had to guess a few cells. This proves that puzzles designed for human players are meant to be solved via logical deduction, making them computationally "easy."

It turns out Sudoku is similar. Although some backtracking is still needed, classic puzzles are typically solved within 100~200 µs (microseconds), while variants might take a few milliseconds. I did see one puzzle take ~20 seconds, but overall, I was happy with the result.

So, can it go faster? Two optimization options came to mind:

1. When a cell changes, only consult relevant constraints rather than re-checking all of them.
2. Instead of copying the entire board state for every guess, I could carefully track changes and undo them during backtracking. However, since the board state is already quite small, I doubted this would yield a significant performance boost in practice.

Right before I decided to optimize further, I learned something new.

3. Dancing Links (DLX)

I discovered "Dancing Links" while asking an AI for the best Sudoku algorithms. This is a technique invented by Donald Knuth to efficiently implement Algorithm X, which solves the "exact cover" problem.

This is perfect for classic Sudoku, where the goal is to find an exact cover between "putting a digit in a cell" and "satisfying every row, column, and box constraint."

This is perfect for the classic Sudoku algorithm, where we essentially try to find the exact cover between "putting a digit into each cell" and "each row/column/box must contain exactly one digit X (where X is 1 ~ 9)".

The magical part: We can precisely undo this process by restoring the covered rows and columns. This means we don't need to copy the state during backtracking! The algorithm only needs to remember the latest guess; the data structure itself holds the information required to reverse it.

However, there's a catch: things get complicated quickly with variant rules. Only a few rules (like distinct values) can be easily encoded into the DLX structure. For most others, I had to implement them as "external observers" that eliminate impossible candidates after a guess. This forced me to maintain an undo stack again, essentially plugging a constraint propagation engine back into DLX.

Another issue: DLX wasn't actually faster than my custom constraint propagation solver. Since it consistently took ~200 µs for classic puzzles, I didn't bother implementing the complex variant rules for it.

4. Generic Solvers

I talked to a colleague about my progress, and he asked, "Why are you writing a custom solver? Why not just use a generic SAT/SMT solver like Z3?"

That was a good point. I did some quick research and picked three candidates to test:

• Z3
• cvc5
• OR-Tools

The results are shown below.

5. Results

Here is how the solvers compared. (cp = my constraint propagation implementation, dlx = my dancing links implementation)

Classic Sudoku 1 (Easy)

• cp: ~100 µs
• dlx* ~200 µs
• OR-Tools: ~10 ms
• Z3: ~20 ms
• cvc5: ~70 ms

Classic Sudoku 2 (Harder)

• cp: ~200 µs
• dlx: ~200 µs
• OR-Tools: ~10 ms
• Z3: ~80 ms
• cvc5: ~200 ms

Hard: Empty Board + Thermometer Rules

• cp: ~3 ms
• OR-Tools: ~30 ms
• Z3: ~20 s
• cvc5: ~23 s

Hard: Almost Empty Board + Arrow Rules

• OR-Tools: ~200 ms (slightly faster than cp)
• cp: ~200 ms
• Z3: ~20 s
• cvc5: ~100 s

6. Discussion

I found these results both surprising and reasonable.

OR-Tools is significantly faster than Z3 and cvc5. I believe this is because OR-Tools uses a CP-SAT (Constraint Programming) solver, whereas Z3 and cvc5 are primarily SMT (Satisfiability Modulo Theories) solvers. Since the Sudoku puzzles I used are designed for human logic, they align better with the constraint propagation techniques used by OR-Tools.

My custom solver vs. OR-Tools. For easy puzzles, OR-Tools is slower than my implementation. This is likely due to initialization overhead; my code is hyper-optimized specifically for Sudoku. However, OR-Tools catches up quickly on complex puzzles. My constraint propagation logic is naturally inferior to the sophisticated heuristics inside OR-Tools, so as complexity rises, the generic solver wins.

7. Conclusion

I had a lot of fun and learned a great deal during this process. My next step is to explore OR-Tools further. Perhaps I'll write solvers for even more complex puzzles without reinventing the wheel!