|
Size: 5303
Comment:
|
← Revision 48 as of 2013-02-11 12:49:28 ⇥
Size: 10971
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 2: | Line 2: |
| Line 7: | Line 6: |
| * [[#checker|Checker Format]] | * [[#checker|Checker Description]] * [[#generator|Generator Description]] |
| Line 10: | Line 10: |
| Line 11: | Line 12: |
* '''Preliminary submission''' (see [[#package-example|Example]]) can be done by providing problem name and problem specification only; we encourage to provide a problem encoding and sample instances also. * '''Complete problem specifications''' (see [[#package-example|Example]]) shall be sent by email to [[mailto:aspcomp_benchmarks_REPLACE_WITH_AT_mat.unical.it|Benchmark Submission]] and have to be packaged in a single compressed archive named {{{benchmark_name-contributor_name.zip}}} (or {{{tar.gz}}}) containing: 1. a {{{benchmark_name.spec.txt}}} file containing the textual problem description (a template is available, see below); 2. a {{{benchmark_name.enc.asp}}} file containing a proposed encoding in ASP for the problem (optional: this is strongly encouraged for problems to be submitted to the System Track); 3. 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; 4. a folder named {{{samples}}} containing some instances (one instance per text file). {{{benchmark_name}}} and {{{contributor_name}}} should be substituted with their actual value. |
* '''Preliminary submission''' --((see [[#package-example|Example]]) simply requires problem name and description/specification only, even if the submission of sample instances is encouraged. In case you want to propose the problem for the System Competition, an ASP encoding is also strongly suggested. If possible, please also mention the complexity of your problem.)-- {{{#!wiki caution Preliminary submissions are now over. Complete problem submissions are now reserved to selected problem authors. }}} * '''Complete problem specifications''' (see [[#package-example|Example]]): Final package submissions are handled by submitting the problem package via Easychair ([[https://www.easychair.org/conferences/?conf=aspcomp2013|here]]), packaged in a single compressed archive named {{{benchmark_name-contributor_name.zip}}} containing: 1. a {{{specification.txt}}} file containing the textual problem description, with a clear specification of the input and output formats. Names and arguments of input and output predicates must be clearly specified (see [[#package-io|Problem I/O]], a template example is also available, see below); 1. a file {{{encoding.asp }}}containing a proposed encoding in ASP for the problem (only required for the System Competition); 1. a folder named {{{checker}}} containing a startup file {{{checker.sh }}}and possibly further sources of a correctness checker (see [[#checker|Checker Description]] for details); 1. a folder named {{{instances}}} containing at least 50 instances instances (one instance per text file, following our [[#MAXINT-MAXLEVEL|instance naming convention]]) or the generator thereof (together with a {{{README.txt}}} that provides instructions for building and running it, see [[#generator|Generator Description]]); 1. a folder named {{{example}}} containing a satisfiable example instance {{{instance.asp }}} and the expected outcome {{{outcome.txt}}}'' ''in order to help in disambiguating blurred specifications. |
| Line 26: | Line 24: |
| Line 27: | Line 26: |
| * ''Sample Package Download'' [[attachment:GraphColouring.zip||&do=get]] * ''Preliminary Submission Example'' [[attachment:GraphColouringPreliminary.zip||&do=get]] |
* ''Preliminary Submission Example'' [[attachment:GraphColouringPreliminary.zip||&do=get]] * ''Complete Submission Example'' [[attachment:GraphColouring.zip||&do=get]] '''Changelog''': * February 11, 2013: fixed (and added) specification for checkers of optimization problems * October 23, 2012: fix compatibility with gringo and lparse |
| Line 31: | Line 35: |
| == Problem Input-Output predicates and Instance Specification == | |
| Line 33: | Line 36: |
| 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-Output predicates and Instance Specification (mandatory for the System Competition) == In the following the allowed format for specifying input and output of problems and instances is given. Samples are available in the competition web site. |
| Line 36: | Line 40: |
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}}}). |
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. {{{edge/2}}} denotes the binary predicate {{{edge}}}). |
| Line 40: | Line 43: |
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). Examples: {{{node(a)}}}, {{{edge(a,b)}}}. The terms {{{a}}} and {{{b}}} can be positive integers, double quoted strings or unquoted strings belonging to the vocabulary {{{[a-zA-Z][a-zA-Z0-9]*}}}. |
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 (instances and files must be in 1-to-1 correspondence). Examples of facts: {{{node(a)}}}, {{{edge(a,b)}}}. The terms {{{a}}} and {{{b}}} can be positive integers, double quoted strings or unquoted strings belonging to the vocabulary {{{[a-zA-Z][a-zA-Z0-9]*}}}. |
| Line 46: | Line 46: |
| ==== 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). These data should be provided for those solvers needing an explicit bound on the range of integers and/or function symbols. One or both can be set to ''0'' if your problem domain does not use either numbers or function symbols or both. |
===== 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). These data should be provided for those solvers needing an explicit bound on the range of integers and/or function symbols. One or both can be set to ''0'' if your problem domain does not use either numbers or function symbols or both. |
| Line 50: | Line 51: |
| == Checker format == The checker reads from standard input a witness (an answer to the problem instance at hand) 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 whenever the output {{{INCONSISTENT}}} has been incorrectly piped towards the checker). Informative messages can be output in standard error. |
|
| Line 53: | Line 52: |
| Note that witnesses given in input to checkers are assumed to be inclusive of both instance facts (input predicates) and solution facts (output predicates). | == Checker Description == The checker gets as parameters |
| Line 55: | Line 55: |
| '''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}}}, or optimality. | 1. the exit code from the solver, which is 10 for satisfiable instances, 20 for unsatisfiable instances, and any other value in case of an error (e.g. timeout, segmentation fault, etc.) 1. the file name of the problem instance |
| Line 57: | Line 58: |
| 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. | If the solver exit code is 10, the checker reads from standard input a witness, i.e. an answer to the problem instance at hand. If the solver exit code is 20, it reads from standard input the constant string {{{INCONSISTENT}}}. If the solver exit code is any other value, it reads from standard input the constant string {{{INCOMPLETE}}}. To sum it up, the checker is called in the following way: ./checker.sh EXITCODE INSTANCEFILE < AS-SOLVER-OUTPUT The checker is expected to write to standard output a single row of text containing the string {{{OK}}} with exit code 0 if the solver exit code and standard input correspond to the expected output for the given instance. That is, the instance is satisfiable and the solver correctly returned 10 and produced an answer set, or the instance is unsatisfiable and the solver correctly returned 20 and the input to the checker was {{{INCONSISTENT.}}}The checker is expected to write a single row of text containing the string {{{FAIL}}} with exit code 1 if the solver result was wrong. That is, e.g., the solver produced an answer set of an inconsistent instance or returned 20 for a satisfiable one. For optimization problems, the checker must also verify the costs claimed by the solver and write {{{FAIL}}} with exit code 1 if a discrepancy is found. '''Remark:''' Additionally, the checker may return 2 and the string {{{DONTKNOW}}} if the checker is not able to verify or falsify the solver result. This result should be avoided whenever possible, but might be used if it is computationally too costly to determine an answer, e.g., to verify an {{{INCONSISTENT }}}result (i.e. to prove that the instance is indeed unsatisfiable) or to prove minimality of an answer set of a disjunctive program. Furthermore, the checker can return {{{WARN}}} and exit code 3 in case an internal checker error occurs. For example, this may be the case when exit code 10 is provided but the given answer set contains a syntactic error or the checker fails due to any unexpected reason. The intuition behind {{{WARN}}} is to detect faulty behavior (i.e. errors that are not related to the correctness of a result but to bugs or noncompliance to the ASP-Competition specifications) of a checker or participating asp solver. In summary, the following cases are possible: ||||<tablewidth="851px" tableheight="160px"style="text-align:center">'''Solver<<BR>>''' ||||<style="text-align:center">'''Checker<<BR>>''' || ||''exit code<<BR>>'' ||''standard output<<BR>>'' ||''standard input<<BR>>'' ||''possible outputs<<BR>>'' || ||10 ||an answer set (including costs for optimization problems) ||an answer set (including costs for optimization problems, see [[#opt-checker|here]]) ||{{{OK }}}with exit code 0 if the answer set is correct; {{{FAIL }}}with exit code 1 if the answer set is incorrect; {{{DONTKNOW }}}with exit code 2 if the checker cannot verify the result; {{{WARN}}} with exit code 3 if there is an internal error || ||20 || ||{{{INCONSISTENT}}} ||{{{OK }}}with exit code 0 if the instance is indeed inconsistent; {{{FAIL }}}with exit code 1 if the instance is consistent; {{{DONTKNOW }}}with exit code 2 if the checker cannot verify the result; {{{WARN}}} with exit code 3 if there is an internal error || ||any other value different from 0 || ||{{{INCOMPLETE}}} ||{{{FAIL }}}with exit code 1; {{{WARN}}} with exit code 3 if there is an internal error || Note that witnesses given in input to checkers are assumed to be inclusive of both instance facts (input predicates) and solution facts (output predicates), but the file name of the instance is additionally passed as second parameter to the checker. The source code of the correctness checker has to be be included in the package; the provided software must be able to (be built 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. <<Anchor(opt-checker)>> ==== Additional Checker Output For Optimization Problems ==== For optimization problems it is necessary that the checker additionally computes the quality of the provided answer set. In case the solver exit code is 10 and the answer set is indeed a solution of the problem, the checker must write to standard output a single row of text containing the string {{{OK}}} followed by a list of costs per level (priority) in the format COSTS@LEVEL. LEVEL is a non-negative Integer. A higher level gives higher priority to the corresponding costs. The least-important level must be specified with LEVEL=0. Each level from least to most important must get assigned costs. Example: {{{OK 20@0 3@1 1@2}}} specifies that the costs at (most prioritized) level 2 are 1, at level 1 the costs are 3 and at the least prioritized level 0 they are 20. |
| Line 61: | Line 93: |
| Line 62: | Line 95: |
| * ''ASP-based Checker Download'' [[attachment:SampleChecker.zip||&do=get]] | * An example checker is contained in the ''Complete Submission Example'': [[attachment:GraphColouring.zip||&do=get]] <<Anchor(generator)>> == Generator Description == The generator should create one instance per call, printing it to standard out. The file {{{README.txt}}} must explain how the instance generator is built and run. In particular, the parameters which may influence the hardness of the instance need to be described, such that we can produce useful benchmark instances ranging from easy to difficult ones. Furthermore, it must describe how the maximum integer and maximum function nesting level are obtained for a generated instance. This allows us to generate instances according to the naming conventions (see [[#MAXINT-MAXLEVEL|instance naming convention]]). In case any of those values are irrelevant for your problem, please mention that the respective value(s) can be set to 0. |
Problem Submission Specification: Input, Output, Checking
Quick Directions
Package Submission Instructions
Preliminary submission (see Example) simply requires problem name and description/specification only, even if the submission of sample instances is encouraged. In case you want to propose the problem for the System Competition, an ASP encoding is also strongly suggested. If possible, please also mention the complexity of your problem.
- Preliminary submissions are now over. Complete problem submissions are now reserved to selected problem authors.
Complete problem specifications (see Example): Final package submissions are handled by submitting the problem package via Easychair (here), packaged in a single compressed archive named benchmark_name-contributor_name.zip containing:
a specification.txt file containing the textual problem description, with a clear specification of the input and output formats. Names and arguments of input and output predicates must be clearly specified (see Problem I/O, a template example is also available, see below);
a file encoding.asp containing a proposed encoding in ASP for the problem (only required for the System Competition);
a folder named checker containing a startup file checker.sh and possibly further sources of a correctness checker (see Checker Description for details);
a folder named instances containing at least 50 instances instances (one instance per text file, following our instance naming convention) or the generator thereof (together with a README.txt that provides instructions for building and running it, see Generator Description);
a folder named example containing a satisfiable example instance instance.asp and the expected outcome outcome.txt in order to help in disambiguating blurred specifications.
Package Example Download
Preliminary Submission Example GraphColouringPreliminary.zip
Complete Submission Example GraphColouring.zip
Changelog:
- February 11, 2013: fixed (and added) specification for checkers of optimization problems
- October 23, 2012: fix compatibility with gringo and lparse
Problem Input-Output predicates and Instance Specification (mandatory for the System Competition)
In the following the allowed format for specifying input and output of problems and instances is given. 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. edge/2 denotes the binary predicate edge).
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 (instances and files must be in 1-to-1 correspondence). Examples of facts: node(a), edge(a,b). The terms a and b can be positive integers, double quoted strings or unquoted strings belonging to the vocabulary [a-zA-Z][a-zA-Z0-9]*.
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). These data should be provided for those solvers needing an explicit bound on the range of integers and/or function symbols. One or both can be set to 0 if your problem domain does not use either numbers or function symbols or both.
Checker Description
The checker gets as parameters
- the exit code from the solver, which is 10 for satisfiable instances, 20 for unsatisfiable instances, and any other value in case of an error (e.g. timeout, segmentation fault, etc.)
- the file name of the problem instance
If the solver exit code is 10, the checker reads from standard input a witness, i.e. an answer to the problem instance at hand. If the solver exit code is 20, it reads from standard input the constant string INCONSISTENT. If the solver exit code is any other value, it reads from standard input the constant string INCOMPLETE.
To sum it up, the checker is called in the following way:
./checker.sh EXITCODE INSTANCEFILE < AS-SOLVER-OUTPUT
The checker is expected to write to standard output a single row of text containing the string OK with exit code 0 if the solver exit code and standard input correspond to the expected output for the given instance. That is, the instance is satisfiable and the solver correctly returned 10 and produced an answer set, or the instance is unsatisfiable and the solver correctly returned 20 and the input to the checker was INCONSISTENT.The checker is expected to write a single row of text containing the string FAIL with exit code 1 if the solver result was wrong. That is, e.g., the solver produced an answer set of an inconsistent instance or returned 20 for a satisfiable one. For optimization problems, the checker must also verify the costs claimed by the solver and write FAIL with exit code 1 if a discrepancy is found.
Remark: Additionally, the checker may return 2 and the string DONTKNOW if the checker is not able to verify or falsify the solver result. This result should be avoided whenever possible, but might be used if it is computationally too costly to determine an answer, e.g., to verify an INCONSISTENT result (i.e. to prove that the instance is indeed unsatisfiable) or to prove minimality of an answer set of a disjunctive program.
Furthermore, the checker can return WARN and exit code 3 in case an internal checker error occurs. For example, this may be the case when exit code 10 is provided but the given answer set contains a syntactic error or the checker fails due to any unexpected reason. The intuition behind WARN is to detect faulty behavior (i.e. errors that are not related to the correctness of a result but to bugs or noncompliance to the ASP-Competition specifications) of a checker or participating asp solver.
In summary, the following cases are possible:
Solver |
Checker |
||
exit code |
standard output |
standard input |
possible outputs |
10 |
an answer set (including costs for optimization problems) |
an answer set (including costs for optimization problems, see here) |
OK with exit code 0 if the answer set is correct; FAIL with exit code 1 if the answer set is incorrect; DONTKNOW with exit code 2 if the checker cannot verify the result; WARN with exit code 3 if there is an internal error |
20 |
|
INCONSISTENT |
OK with exit code 0 if the instance is indeed inconsistent; FAIL with exit code 1 if the instance is consistent; DONTKNOW with exit code 2 if the checker cannot verify the result; WARN with exit code 3 if there is an internal error |
any other value different from 0 |
|
INCOMPLETE |
FAIL with exit code 1; WARN with exit code 3 if there is an internal error |
Note that witnesses given in input to checkers are assumed to be inclusive of both instance facts (input predicates) and solution facts (output predicates), but the file name of the instance is additionally passed as second parameter to the checker.
The source code of the correctness checker has to be be included in the package; the provided software must be able to (be built 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.
Additional Checker Output For Optimization Problems
For optimization problems it is necessary that the checker additionally computes the quality of the provided answer set. In case the solver exit code is 10 and the answer set is indeed a solution of the problem, the checker must write to standard output a single row of text containing the string OK followed by a list of costs per level (priority) in the format COSTS@LEVEL. LEVEL is a non-negative Integer. A higher level gives higher priority to the corresponding costs. The least-important level must be specified with LEVEL=0. Each level from least to most important must get assigned costs. Example: OK 20@0 3@1 1@2 specifies that the costs at (most prioritized) level 2 are 1, at level 1 the costs are 3 and at the least prioritized level 0 they are 20.
Checker Example Download
An example checker is contained in the Complete Submission Example: GraphColouring.zip
Generator Description
The generator should create one instance per call, printing it to standard out.
The file README.txt must explain how the instance generator is built and run. In particular, the parameters which may influence the hardness of the instance need to be described, such that we can produce useful benchmark instances ranging from easy to difficult ones.
Furthermore, it must describe how the maximum integer and maximum function nesting level are obtained for a generated instance. This allows us to generate instances according to the naming conventions (see instance naming convention). In case any of those values are irrelevant for your problem, please mention that the respective value(s) can be set to 0.