A closely related technique to SAT solvers is the "Constraint Satisfaction Problem" which I've been looking into recently.<p>Constraint Programming and SAT are BOTH NP-complete problems, and as such, they are mathematically equivalent. However, its sometimes more "obvious" to write problems in one form vs the other.<p>For example, Sudoku is simply written 27 constraints:<p>* All Different (X11, X12, X13, X14, X15, X16, X17, X18, X19)<p>* All Different (X21, X22, X23, X24, X25, X26, X27, X28, X29)<p>...<p>* All Different (X11, X21, X31, X41, X51, X61, X71, X81, X91)<p>...<p>* All Different (X11, X12, X13, X21, X22, X23, X31, X32, X34)<p>...<p>etc. etc.<p>Then define each "X" variable as "between 1 and 9" and bam, you're done with defining the problem in terms of "Constraints".<p>Representing Sudoku as a SAT problem is possible of course, but its just... harder. It just feels more humanly natural to represent Sudoku in terms of constraints. Or maybe not. Read "Part 1" if you want to see how the original blogger solved it in terms of 3-SAT (<a href="https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/" rel="nofollow">https://codingnest.com/modern-sat-solvers-fast-neat-underuse...</a>)<p>----------<p>Here's an article from IBM hyping up their "CPLEX" Constraint solver for Sudoku for example: <a href="https://www.ibm.com/developerworks/community/blogs/jfp/entry/solving_the_hardest_sudoku?lang=en" rel="nofollow">https://www.ibm.com/developerworks/community/blogs/jfp/entry...</a><p>----------<p>Anyway, just plugging in a similarly fast, neat, and underused (and mathematically equivalent) solver to what the blogpost talks about. I personally don't know too much about SAT-solvers or their algorithms, aside from "They're same same, but different" to Constraint Programming.