[riku_iki]

> Add to this that propositional logic (the language in which we express SAT) is a versatile language to code problems in

is it though? You can't express some basic loop in propositional logic, right?

[viraptor]

Loops are part of a coded solution, not the problem. With SAT you encode the problem / solution space itself.