[viraptor]

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