[lamchob]

The general method presented here is Constraint Programming (CP), a sibling of SAT and ILP. In CP, you can formulate constraints over variables. Search is then performed branch-n-bound style. A variable is assigned, then constraints check if the assignment is legal and remove non-solutions from the other variable's domains.

If anyone is interested: An accessible python module for this is python-constraint. Gecode is a powerful, modern C++ CP Framework.

[mzl]

Here is the send more money puzzle in Gecode: https://github.com/Gecode/gecode/blob/develop/examples/money...

[zshrdlu]

Here in a 30-year-old Common Lisp library: https://unwindprotect.com/constraint-programming

[dragontamer]

And this exists because all of these problems are NP-complete, so "guess-and-check" is basically the state-of-the-art right now. CP, ILP, and 3SAT all can be converted into each other, so if you can find a faster algorithm than guess-and-check, you'll probably improve the state of the art.

[mzl]

All of CP, SAT, and ILP are much more advanced than guess and check, although there are never any guarantees.

[dragontamer]

IMO, "guess and check" describes WalkSAT and Backtracking (including DPLL) pretty effectively.

There's a lot of nuance in exactly how you're guessing-and-checking. But... its a pretty good idea. In the case of Backtracking-search with lookahead, the "guess" is your initial label / variable assignment. When it doesn't work out, maybe you perform some kind of "learning" over the guess (why didn't it work? Can it be written into a new constraint?), and then you guess again (aka: backtracking search).

When you're out of heuristics (variable-ordering heuristics, domain ordering heuristics, etc. etc.) , your best improvement is to arbitrarily choose another variable + assignment and see if it works out. When it doesn't work, you backtrack a bit and guess again with the new information you gathered.

[mzl]

You are missing the crucial role of propagation - looking at the current state and making inferences based on that. Admittedly, DPLL is pretty weak on that with “just” unit propagation, but it is still _very_ important.

[dragontamer]

If you told someone to "Guess-and-check" a Sudoku puzzle, they will innately "learn" about the puzzle from their guesses.

The question of "guess-and-check" is "how much time should I spend making a good guess" ?? If you spend a lot of time making inferences, you're doing "Strong guess and check".

If you spend almost no time making inferences, you're doing "weak guess and check".

--------

People who play Suduku puzzles know that "weak guess and check" solves easier puzzles faster, but "strong guess and check" solves harder puzzles faster. And worst of all, there's no way to really know if you have a hard or easy puzzle ahead of time.

So I argue that "guess and check" is a good layman's term for this whole affair. What you're calling "inference" and "unit propagation" are just the "strength of the guess"... the amount of time you spend thinking about your guess before dedicating yourself to it.

[mzl]

Guess-and-check is usually another term for generate-and-test, which explicitly does not do propagation.

[freemint]

Not all ILP can be converted to SAT, unbounded integers can not be processed in one SAT problem without Infinite formulas

[freemint]

You missed another sibling: Pseudo Boolean Programming