Various sorts of scheduling problems come to mind... for example compilers can make good use of a fast sat solver; but typically you want a failover heuristic so you won't spend forever on large or unsolvable problems