|
Size: 4702
Comment:
|
Size: 4662
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 54: | Line 54: |
The checker reads from standard input a witness in the prescribed format (see [[http://www.mat.unical.it/aspcomp2011/files/LanguageSpecifications.pdf|File and Language Format]] for details) and writes in standard output a single row of text containing the string {{{OK}}} (if the witness is correctly assessed as a solution), and the string {{{FAIL}}} otherwise. The string {{{OK}}} must be followed by a space-separated integer representing the witness cost in case of optimization problems. The checker outputs {{{WARN}}} and an exit code different from zero in all other cases (e.g. the witness is not syntactically correct, or the output {{{INCONSISTENT}}} has been incorrectly piped towards the checker). Informative messages can be output in standard error. |
The checker reads from standard input a witness and writes in standard output a single row of text containing the string {{{OK}}} (if the witness is correctly assessed as a solution), and the string {{{FAIL}}} otherwise. The string {{{OK}}} must be followed by a space-separated integer representing the witness cost in case of optimization problems. The checker outputs {{{WARN}}} and an exit code different from zero in all other cases (e.g. the witness is not syntactically correct, or the output {{{INCONSISTENT}}} has been incorrectly piped towards the checker). Informative messages can be output in standard error. |
| Line 61: | Line 58: |
| '''Remark''': checkers provided by benchmark authors will be used only for checking existing witnesses. It is not up to the benchmark author to check validity of other outputs like {{{INCONSISTENT}}}. |
'''Remark''': checkers provided by benchmark authors will be used only for checking existing witnesses. It is not up to the benchmark author to check validity of other outputs like {{{INCONSISTENT}}}. |
| Line 65: | Line 61: |
'''Remark''': the development of checkers in form on ASP programs is preferable and strongly encouraged. |
Problem Submission Specification: Input, Output, Checking
Quick Directions:
- Input, Ouput and Instance Specification
- Package Submission Templates
- Checker Format
Package Submission Templates
Preliminary submission (see Example) can be done by providing problem name and problem specification only; we encourage to provide an ASP encoding and sample instances also.
Complete problem specifications (see Example) shall be sent by email to Benchmark Submission enclosed in a single compressed package (zip, rar, and tar.gz are allowed formats), containing:
have to be packaged in a single compressed archive named benchmark_name-contributor_name.zip (or tar.gz) containing:
a benchmark_name.spec.txt file containing the textual problem description (a template is available, see below);
a benchmark_name.enc.asp file containing a proposed encoding in ASP for the problem (details about the language will follow);
a folder named checker containing the sources of a correctness checker together with a README.txt file containing the instructions for (possibly building and) running it;
a folder named samples containing some instances (one instance per text file).
benchmark_name and contributor_name should be substituted with their actual value.
Package Example Download
Sample Package Download GraphColouring.zip
Preliminary Submission Example GraphColouring.txt
Problem Input-Output predicates and Instance Specification
In the following it is specified the allowed format for specifying input and output of problems and instances. Samples are available in the competition web site.
Problem Input and Output.
Benchmark problems specifications have to clearly indicate the vocabulary of input and output predicates, i.e., a list of predicate names for the input and a list of predicate names for the output and their arity in the usual logic programming notation (e.g. p/2 denotes the binary predicate p).
Instance Specification.
Input instance are sequences of Facts (atoms followed by the dot "." character) with only predicates of the input vocabulary, possibly separated by spaces and line breaks, entirely saved in a text file (only one instance per file is allowed).
Maximum Integer and maximum function nesting level,
have to be provided in a per-instance basis. In particular, they are specified in the filename containing a given instance. We recall that instances must be named XX-benchmark_name-MAXINT-MAXLEVEL.asp where XX is the instance number, MAXINT is the maximum integer (0 if not relevant/no arithmetics are required), and MAXLEVEL is the maximum function nesting level (0 if not relevant).
Checker format
The checker reads from standard input a witness and writes in standard output a single row of text containing the string OK (if the witness is correctly assessed as a solution), and the string FAIL otherwise. The string OK must be followed by a space-separated integer representing the witness cost in case of optimization problems. The checker outputs WARN and an exit code different from zero in all other cases (e.g. the witness is not syntactically correct, or the output INCONSISTENT has been incorrectly piped towards the checker). Informative messages can be output in standard error.
Note that witnesses are assumed to be inclusive of both instance facts (input predicates) and solution facts (output predicates).
Remark: checkers provided by benchmark authors will be used only for checking existing witnesses. It is not up to the benchmark author to check validity of other outputs like INCONSISTENT.
The source code of the correctness checker has to be be included in the package; moreover, the provided software must be able to (build and) run on the Debian i686 GNU/Linux(kernel ver. 2.6.26) operating system. A checker can be built on top of a logic specification for a solver of choice: in such a case binaries of the solver must be provided together with the checker encoding.
Remark: the development of checkers in form on ASP programs is preferable and strongly encouraged.