Output Format

[jardinetsouffleton]

Output Format

To communicate their answers, solvers must print messages to the standard output and those messages will be used to check the results. The first two characters of a line allow us to classify it into different categories, which indicate the meaning of the line. With the exception of "o " lines, there is no specific order imposed on the lines output by solvers.

Status line

This line starts with the two characters: lower case s followed by a space (ASCII code 32).
Only one such line is allowed, and it is mandatory.
Possible status:

s UNSUPPORTED
s SATISFIABLE
s OPTIMUM FOUND
s UNSATIFIABLE
s NKNOWN

If the solver does not output a status line, or if the status line is misspelled, then UNKNOWN will be assumed.

Values line

Starts with the two characters: lower case v followed by a space (ASCII code 32).
It is mandatory when the instance is satisfiable.
More than one "v " line is allowed.
Solutions must respect the format described in Section 2.11 of [BLAP22].
Example:

v <instantiation type="solution">
v <list> x[] </list>
v <values> 1 1 2 * </values>
v </instantiation>

v <instantiation>
v <list> b c </list>
v <values> 2 2 </values>
v </instantiation>

v <instantiation>
v <list> x[] </list>
v <values> 1 1 2 * </values>
v </instantiation>

Objective line

Starts with the two characters: lower case o followed by a space (ASCII code 32).
These lines are mandatory for incomplete solvers, but not strictly mandatory for complete solvers.
An "o " line must contain the lower case o followed by a space and then by an integer that represents the better value of the objective function.

Example of the final output:

o 450
o 1700
s OPTIMUM FOUND
v <instantiation> <list> b c </list> <values> 2 2 </values> </instantiation>

Examples

For example outputs, refer to the original document.