Specific rules for CSP Solvers

A CSP solver must output exactly one 's ' line (it is mandatory) and in addition, when the instance is found SATISFIABLE, exactly one 'v ' line. These lines are not necessarily the first ones in the output since the CSP solver can output some 'c ' and 'd ' lines in any order. For a CSP solver, the 's ' line must correspond to one of the following answers:

s UNSUPPORTED:

when the solver recognises an instance with a constraint not implemented;

s SATISFIABLE:

when the solver has found a solution;

s UNSATISFIABLE:

when the solver can prove that the instance has no solution;

s UNKNOWN:

when the solver is not able to tell anything about the instance.

If the solver does not output a 's ' line, or if the 's ' line is misspelled, then UNKNOWN will be assumed. For a CSP solver, the 'v ' line provides a valuation of each variable that satisfies all constraints. This will be used to check the correctness of the answer.