Output Format
All solver output on stdout must either be a
comment line, a
solution line, or a
value line.
Comment lines start with a lower case "c" followed by a space.
Comments are optional and may appear anywhere in the solver output.
The solution line is mandatory and must appear exactly once.
The solution line starts with a lower case "s" followed by a space.
It must be one of the following answers:
- s SATISFIABLE
This indicates that the solver has found a model of the formula.
In such a case, and if the track requires satisfying assignments, the output of one or multiple value lines is mandatory.
- s UNSATISFIABLE
This indicates that the solver has proof that the formula has no model.
In such a case, and if the track requires UNSAT certificates, the proof must be written to a file called "proof.out".
- s UNKNOWN
This line must be output in any other case, i.e. when the solver is not able to tell anything about the formula.
Satisfying Assignment
Value lines start with a lower case "v" followed by a space.
Values are given as a space-separated list of non-contradictory literals.
The negation of a literal is denoted by a minus sign immediately followed by the identifier of the variable.
At least one literal of every clause needs to appear in the value lines.
Note that partial satisfying assignments are allowed.
The order of the literals does not matter.
Value lines can have at most 4096 characters.
So for most problems multiple value lines are necessary.
The last value line must be terminated by a "0" (zero) to indicate the end of the satisfying assignment.
Certificates of Unsatisfiablity
All participants in the Main track of this competition must output proofs of unsatisfiabiliy, which must be written to a file called
proof.out.
Depending on which of the proof checkers DPR, GRAT or VeriPB is selected,
proof.out is input to dpr-trim, gratgen or veripb respectively.
The pipelines of verified proof checkers that we provide on StarExec are described in the following documents.