Ok, in this specific case, a puzzle with what 10 pieces, a recursive backtracker will be just as fast and more importantly, be far easier to reason about and implement.
If this was a thousand piece puzzle, I would still venture recursive backtracker with good heuristics will beat CP-SAT, even in the sudoku case some good heuristics with backtracking beats CP-SAT. Not sure why Claude immediately jumped to using CP-SAT.
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.
taeric 49 minutes ago [-]
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.
nh23423fefe 4 hours ago [-]
> It was much better than I would have written myself, and I ended up learning from it.
Eventually shitting on LLM code will be seen by all as lazy cope. I too am aware of the existence of SAT but I really would struggle to immediately see through some problem i was having and interpret SAT unless I did it a bunch. Having agent suggest the "right thing" is clearly better. And hopefully would help my intuition in the future.
akoboldfrying 4 hours ago [-]
> Instead of backtracking, Claude just imported an industrial-strength library made to solve these sorts of problems. OR-Tools CP-SAT is put out by Google and is made for solving constrained optimization problems, as well as satisfiability problems like this one.
I'm not familiar with CP-SAT, but TTBOMK all SAT solvers use a type of backtracking search underneath called DPLL. Modern ones are highly tuned in terms of which variable they choose to branch on next, and in what order to try its possible values; this can have an enormous impact on runtime. They probably use several tricks on top of that; the big one that I'm aware is conflict-driven clause learning, where the solver adds new constraints that it discovers as it goes along (e.g., it might be able to determine that x and y always have the same value in every solution), which can shrink the search space a lot.
taeric 46 minutes ago [-]
Yes, constraint learning is a huge deal. And there is a fun trick to solving sudoku that is basically this. Someone realized that you can essentially build an extra ring around the board that has the same constraints as elsewhere. Phistomefel Ring is the name, I believe. (This may be a different one, I just reached for the first thing a google search found for my vague description.)
https://en.wikipedia.org/wiki/Constraint_satisfaction_proble...
If this was a thousand piece puzzle, I would still venture recursive backtracker with good heuristics will beat CP-SAT, even in the sudoku case some good heuristics with backtracking beats CP-SAT. Not sure why Claude immediately jumped to using CP-SAT.
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.
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.
Eventually shitting on LLM code will be seen by all as lazy cope. I too am aware of the existence of SAT but I really would struggle to immediately see through some problem i was having and interpret SAT unless I did it a bunch. Having agent suggest the "right thing" is clearly better. And hopefully would help my intuition in the future.
I'm not familiar with CP-SAT, but TTBOMK all SAT solvers use a type of backtracking search underneath called DPLL. Modern ones are highly tuned in terms of which variable they choose to branch on next, and in what order to try its possible values; this can have an enormous impact on runtime. They probably use several tricks on top of that; the big one that I'm aware is conflict-driven clause learning, where the solver adds new constraints that it discovers as it goes along (e.g., it might be able to determine that x and y always have the same value in every solution), which can shrink the search space a lot.