← Back to context

Comment by nextaccountic

3 months ago

On same level of abstraction I think it's useful to view those tools as some form of constraint solving. Think how you can solve sudoku with pen and paper by writing out each possibility, then fill squares either because it has only one possibility or by making guesses. After you fill a square, you can then update your possible states (propagate constraints), and repeat until you solve it or hit an impossible solve (in which case you need to backtrack on some earlier guess).

The algorithms differ mainly in how they keep track of all possibilities and how they update them

I think this answer is pretty good https://cstheory.stackexchange.com/a/29428 (take note at the end "sat is csp on boolean domains")