welcome: please sign in
location: Diff for "ProblemIOSpecification"
Differences between revisions 26 and 27
⇤ ← Revision 26 as of 2012-05-11 10:30:00 →
Size: 5514
Editor: GiovambattistaIanni
Comment:
← Revision 27 as of 2012-08-02 12:00:26 → ⇥
Size: 9000
Editor: ChristophRedl
Comment:
Deletions are marked like this. Additions are marked like this.
Line 2: Line 2:
Line 10: Line 9:
Line 11: Line 11:
Line 13: Line 12:
 * '''Complete problem specifications''' (see [[#package-example|Example]]) must be sent by email to [[mailto:aspcomp_benchmarks_submission@yahoogroups.com|Benchmark Submission]], 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 example is available, see below);
  2. a {{{benchmark_name.enc.asp}}} file containing a proposed encoding in ASP for the problem (optional: but this is strongly encouraged for problems to be submitted to the System Competition);
  3. a folder named {{{checker}}} containing the sources of a correctness checker together with a README.txt, that provides instructions for (possibly building and) running it;
  4. a folder named {{{samples}}} containing instances (one instance per text file) or the generator thereof.

{{{benchmark_name}}} and {{{contributor_name}}} should be substituted with their actual value.		  * '''Complete problem specifications''' (see [[#package-example|Example]]) must be sent by email to [[mailto:aspcomp_benchmarks_submission@yahoogroups.com|Benchmark Submission]], 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 [[ProblemIOSpecification|Problem I/O]]); (a template example is available, see below);
  1. a {{{encoding.asp}}} file containing a proposed encoding in ASP for the problem (only required for thee 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) or the generator thereof (together with a README.txt, that provides instructions for building and running it).
  1. a folder named {{{example}}} containing an example instance {{{instance.asp }}}and the expected outcome {{{outcome.txt}}}'' ''in order to help in disambiguating blurred specifications
  1.
  1. a textual problem description
  1. if the problem has been included into the [[SystemCompetition|System Track]] benchmark suite, a problem encoding in ASP;
  1. , or, equivalently, a script/program that is able to generate problem instances. The format of instances can be found in the [[ProblemIOSpecification|Instance Specification]] page.
  1. a correctness checker, that is, a script or a program (preferably written in ASP whenever possible) that is able to decide whether, given an instance of a the problem at hand, the output of a system actually represent a solution to the instance. If the problem has been included into the System Competition benchmark suite, the ASP program or the script must check whether the predicates occurring in some answer set provided by the system form a solution to the instance. In case of an optimization problem, the program should be also able to compute the "quality" of the answer (see [[ProblemIOSpecification|Checker Specification]]).
  1. a "demonstration", in which the author convincingly shows that the benchmark problem both can be effectively handled/solved and it is not trivial.
 '''Note that''': ''The problem statement must be unambiguous and include the description of input and output according to the problem description format described above. We would really appreciate if you can provide us with a declarative encoding and some sample instance at once: the submission of problems encodings often helps in disambiguating blurred specifications, so its provision is encouraged.''
Line 22: Line 27:
Line 23: Line 29:
  * ''Preliminary Submission Example'' [[attachment:GraphColouringPreliminary.zip||&do=get]]
  * ''Complete Submission Example'' [[attachment:GraphColouring.zip||&do=get]]
  * ''Preliminary Submission Example'' [[attachment:GraphColouringPreliminary.zip||&do=get]]
 * ''Complete Submission Example'' [[attachment:GraphColouring.zip||&do=get]]
Line 28: Line 33:
Line 29: Line 35:

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.  		 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.
Line 34: Line 38:
Line 38: Line 41:

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]*}}}. 		 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 44: Line 44:
Line 45: Line 46:
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.   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 48: Line 49:
== 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 51: Line 50:
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 53: Line 53:
'''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}}} (non-existence of witnesses), or to check 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

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.}}}

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 and 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.

'''Remark:''' Additionally, the checker may return 2 and the string {{{DO_NOT_KNOW}}} 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.

In summary, the following cases are possible:

||||<tablewidth="851px" tableheight="160px">'''Solver<<BR>>'''||||'''Checker<<BR>>'''||
||''exit code<<BR>>''||''standard output<<BR>>''||''standard input<<BR>>''||''possible outputs<<BR>>''||
||10||an answer set||an answer set||{{{OK }}}with exit code 0 if the answer set is correct {{{FAIL }}}with exit code 1 if the answer set is incorrect {{{DO_NOT_KNOW }}}if the checker cannot verify the result ||
||20|| ||{{{INCONSISTENT}}}||{{{OK }}}with exit code 0 if the instance is indeed inconsistent {{{FAIL }}}with exit code 1 if the instance is consistent ||
||any other value|| ||{{{INCOMPLETE}}}||{{{FAIL }}}with exit code 1||


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.
Line 58: Line 76:
Line 59: Line 78:
  * ''ASP-based Checker Download'' [[attachment:SampleChecker.zip||&do=get]]  * ''ASP-based Checker Download'' [[attachment:SampleChecker.zip||&do=get]]

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.

  • Complete problem specifications (see Example) must be sent by email to Benchmark Submission, 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 Problem I/O); (a template example is available, see below);

    2. a encoding.asp file containing a proposed encoding in ASP for the problem (only required for thee System Competition);

    3. a folder named checker containing a startup file checker.sh and possibly further sources of a correctness checker; see Checker Description for details

    4. a folder named instances containing at least 50 instances instances (one instance per text file) or the generator thereof (together with a README.txt, that provides instructions for building and running it).

    5. a folder named example containing an example instance instance.asp and the expected outcome outcome.txt in order to help in disambiguating blurred specifications

    7. a textual problem description

    8. if the problem has been included into the System Track benchmark suite, a problem encoding in ASP;

    9. , or, equivalently, a script/program that is able to generate problem instances. The format of instances can be found in the Instance Specification page.

    10. a correctness checker, that is, a script or a program (preferably written in ASP whenever possible) that is able to decide whether, given an instance of a the problem at hand, the output of a system actually represent a solution to the instance. If the problem has been included into the System Competition benchmark suite, the ASP program or the script must check whether the predicates occurring in some answer set provided by the system form a solution to the instance. In case of an optimization problem, the program should be also able to compute the "quality" of the answer (see Checker Specification).

    11. a "demonstration", in which the author convincingly shows that the benchmark problem both can be effectively handled/solved and it is not trivial.

    Note that: The problem statement must be unambiguous and include the description of input and output according to the problem description format described above. We would really appreciate if you can provide us with a declarative encoding and some sample instance at once: the submission of problems encodings often helps in disambiguating blurred specifications, so its provision is encouraged.

Package Example Download

Problem Input-Output predicates and Instance Specification (mandatory for the System Competition)

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. 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

  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.)
  2. 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.

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 and 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.

Remark: Additionally, the checker may return 2 and the string DO_NOT_KNOW 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.

In summary, the following cases are possible:

Solver

Checker

exit code

standard output

standard input

possible outputs

10

an answer set

an answer set

OK with exit code 0 if the answer set is correct FAIL with exit code 1 if the answer set is incorrect DO_NOT_KNOW if the checker cannot verify the result

20

INCONSISTENT

OK with exit code 0 if the instance is indeed inconsistent FAIL with exit code 1 if the instance is consistent

any other value

INCOMPLETE

FAIL with exit code 1

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.

Checker Example Download

ASP Competition 2013: ProblemIOSpecification (last edited 2013-02-11 12:49:28 by GuentherCharwat)