Remix.run Logo
▲ CJefferson 3 hours ago

I 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.