Input and Output Format

Search Problems

For each benchmark search problem, a participant submits a shell script that calls his solver together with the modeling of the benchmark. This script reads an input instance (from standard input) and produces an output (to standard output) according to the following formats:

• Input: A sequence of atoms with predicates of the input vocabulary. Each atom is followed by "." ,
  a number of spaces and possibly a line break. (See below for an example). An atom has the following format:
  • Atom := Predicate | Predicate(Argument[,Argument]) , where the arity of the predicate matches the number of arguments.
  • Predicate := Word
  • Argument := an integer number (say 12 or -14) or a Word
  • Word :=  sequence of symbols in {a,..,z, 0,..,9,_}, starting with an alphabetical character from {a,..,z}.
• Output: The script will write the following output to standard output:
  • UNSATISFIABLE, in case the instance has no solution;
  • A sequence of atoms of the output vocabulary, representing a "witness" or a model solving the instance problem in case the instance is satisfiable. The format of the sequence is the same as for the input except that it should not contain line breaks.
  • UNKNOWN, if the solver decides to give up before time-out. 

Example.

Optimization problems

An optimization problem is specified as a search problem together with a cost function which assigns an integer cost value to witnesses. We are searching for witnesses with minimal cost. The benchmark script reads an input instance from standard input in the same format as for search problems, and writes output of the following format:

• UNSATISFIABLE, in case of unsatisfiable instances (unlikely to occur).
• A series of witnesses of the search problem, one per line and separated by the return character in case of an satisfiable instance. The witnesses are written on standard output in the same format as for search problems. Only the last (and hopefully best) witness will be considered.
• OPTIMUM FOUND, in case the last produced witness is optimal. This keyword should appear on a new line following the last and optimal witness.   

Example.