Comment by userbinator

Aren't hash functions a counterexample? There have been attempts at using SAT solvers to find preimage and collision attacks on them.