Tekstiviesti: SAT-solving in CSP trace refinement