The reason we don't do this in production is that the solvers take an unpredictable amount of time. A small problem can take forever and a large problem can be instant. You can't gave that in a compiler.

There are enough people at Apple who know about SAT solvers. :)