Compiling problem specifications into SAT