[ComplexSystems]

SAT turns up everywhere because it's almost universal kind of problem. Since it is NP complete, everything in NP can be transformed into an instance of SAT. Since P is a subset of NP, everything in P can be also be turned into an instance of SAT. Nobody knows if things in PSPACE can be, though.

[butokai]

Add to this that propositional logic (the language in which we express SAT) is a versatile language to code problems in. Finding cliques in a graph is also NP complete, but it is less natural to use it as a language to code other problems.

[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.

[CaptainNegative]

> Since P is a subset of NP, everything in P can be also be turned into an instance of SAT.

This statement is kind of trivial. The same is true for any language (other than the empty language and the language containing all strings). The reduction is (1) hardcode the values of one string, y, that is in the language and another string, z, that is not in the language (2) solve the problem on the given input x in polynomial time poly(x) (3) return y if x is to be accepted and z otherwise.

The total running time is at most poly(x)+O(|y|+|z|) which is still poly(x) since |y| and |z| are hardcoded constant values.