alt Hacker NewsI would be shocked if a good recursive backtracker could beat a good SAT solver for large problems. I mean, if you could solve SAT with recursive backtracking people would. That is the core of a SAT or CP solver, with the all the extra clever stuff.
I've spent significant chunks of my career help people throw away backtracking searchers people polished over years with a CP-SAT model I threw together in 30 minutes, often much to their upset.
You can for Sudoku often beat a CP-SAT solver, but that's because the problems are trivial and take milliseconds. If you look at more difficult Sudoku variants, or 16x16 grids, backtracking solvers start to fall behind.
Agreed. I don't know if I would be shocked, but I would be surprised.
This is one that is hard for people to really internalize, I think? The SAT solvers many are likely to use today are not at all the same as the ones they would have used 20 years ago. They have made some amazing advances in how to approach those problems.
There are also probably some very poorly conceived models that people use to adapt a problem to some of these solvers.