Automatic translation to SAT.