I know a little about SAT solvers. I wrote a SAT library, based on MiniSAT, used in production in the Meteor package manager, and more recently I’ve used my SAT solver as part of a sudoku solver that can solve standard Sodukos and also exotic variants, quite efficiently.

While technically, SAT has exponential algorithmic complexity, in practice, SAT solvers can solve problems with thousands of boolean variables quite quickly. “Guess and check” on these same problems would take the lifetime of the universe. CPU vs GPU does not remotely cover the difference.

Basically, I have no idea what this author is going on about, this could be a joke for all I know.