Answer Set Solver Output
========================

Thomas Krennwallner <tkren at kr dot tuwien dot ac dot at>
February 1, 2013

The purpose of this document is to standardize the exit codes and the
output of grounders and solvers for different computational problems
associated with answer set programs.  The tables below represent what
should appear on stdout in the out_i and out_ij lines, and what
should be the respective exit code of the solver in each case.  Solvers
may write warnings, statistics, and debug information on stdout using
comment lines.


Exit Code Bit Encoding
----------------------

Each exit code represents a possibly successful run of a
solver/grounder: based on the exit status, the end user should be able
to answer decision problems without parsing the output, or decide
whether something went wrong or no solution could be found.

Exit codes must fit within the lowest 8 bits of an integer.  In order to
be backward-compatible with SAT/QBF solvers, we use the status values 10
and 20 to encode satisfiable and unsatisfiable instances, respectively.
This gives the following bit patterns for satisfiable and unsatisfiable
runs: 00001010 resp. 00010100.  Furthermore, SAT/QBF solvers may exit
without a known solution (e.g., when they have hit the time/memory
limit), but their exit status do not agree with these kind of runs.

As ASP solvers usually implement many different computational problems,
three exit codes are not enough to give us all information on the exit
status of a solver.  For this reason, we use the following bit scheme to
encode the status of a ground/solver run.

|-------+-------+-------+---------+-------+---------+-------+-------|
| bit 7 | bit 6 | bit 5 | bit 4   | bit 3 | bit 2   | bit 1 | bit 0 |
|-------+-------+-------+---------+-------+---------+-------+-------|
| NORUN | RES1  | RES2  | EXHAUST | SAT   | EXHAUST | SAT   | INT   |
|-------+-------+-------+---------+-------+---------+-------+-------|

The top row of the table denote the position of the bit in a char, and
the bottom row shows the name of the bit.

The highest bit NORUN is used to signal whenever the grounder/solver did
not start the computation.  There could be several reasons, most likely
whenever the input instance is syntactically unsupported, there is a
syntax error, or a command line argument is not known or conflicts with
another one.  Hence, exit code 128 must be used whenever the
grounder/solver process quits without starting the computation.  The
NORUN bit is mutually exclusive with all other bits.

The lowest bit INT encodes that the grounder/solver was being terminated
by the environment (i.e., received a signal) without completing the
computation to the given problem.  This bit must be set in the exit code
of runs where the grounder/solver gets a signal from the environment, or
when computational ressources like time or memory are exhausted.  Thus,
exit status 1 (or 11) is used in runs, where no (complete) solution is
known or where the grounding had been interrupted.  When the solver has
been interrupted during an enumeration task and after enumerating some
models, the exit code will have this bit set to true; those runs
correspond to exit code 11.

The other bits---RES1, RES2, EXHAUST, and SAT---are used for solver runs
that found some solutions to a given problem.  Grounders do not touch
these bits, thus successful grounding runs have exit code 0, which is
important for grounding/solving pipelines.  Setting the SAT bit encodes
that the solver found at least one solution.  The EXHAUST flag is used
to signal that the solver exhaustively went through the search space.
For instance, inconsistent instances have bit EXHAUST and bit SAT set to
1 and 0, resp.: this corresponds to an exit status with value 20.  Bits
RES1 and RES2 are not specified here, they are reserved for future use.
Both of them must be set to 0 whenever INT is 0.  For instance,
implementors may use them to encode further status information for
interrupted runs.  The specified exit codes in this document can be
always retrieved from such exit codes with a bitmask of 0x9f.

We currently have the following exit codes:

|-----------+--------------------------------------------------------------------------------------|
| Exit code | Meaning                                                                              |
|-----------+--------------------------------------------------------------------------------------|
|         1 | Run interrupted: No solution has been found so far                                   |
|-----------+--------------------------------------------------------------------------------------|
|        10 | Program is consistent / some consequences exist / one optimum found / query is true  |
|-----------+--------------------------------------------------------------------------------------|
|        11 | Run interrupted: Program is consistent / some consequences exist                     |
|-----------+--------------------------------------------------------------------------------------|
|        20 | Program is inconsistent / query is false                                             |
|-----------+--------------------------------------------------------------------------------------|
|        30 | Program is consistent, all possible solutions/consequences enumerated / optima found |
|-----------+--------------------------------------------------------------------------------------|
|       128 | Syntax error / command line arguments error                                          |
|-----------+--------------------------------------------------------------------------------------|

The following table summarises the expected behaviour of a solver when
interrupted by one of the following (standard) termination signals:

|-------------+------------------+---------------------+-------------------|
| Reason      | Default action   | Expected action     | Description       |
|-------------+------------------+---------------------+-------------------|
| SIGHUP (1)  | exit(129)        | exit(1) or exit(11) | kill -HUP         |
| SIGINT (2)  | exit(130)        | exit(1) or exit(11) | Ctrl-C            |
| SIGQUIT (3) | exit(131) + core | exit(1) or exit(11) | Ctrl-\            |
|-------------+------------------+---------------------+-------------------|

Further signals are relevant in the context of the ASP Competition 2013.
Here, different signals encode the reason for solver termination.

|--------------+------------------+---------------------+-----------------------------------------------------|
| Reason       | Default action   | Expected action     | Description                                         |
|--------------+------------------+---------------------+-----------------------------------------------------|
| SIGKILL (9)  | exit(137)        | cannot be changed   | sent when process(es) continue to run after timeout |
| SIGSEGV (11) | exit(139)        | exit(1) or exit(11) | sent when memout is reached, or programming error   |
| SIGTERM (15) | exit(143)        | exit(1) or exit(11) | sent at most 10 secs after timeout                  |
| SIGXCPU (24) | exit(152) + core | exit(1) or exit(11) | sent when timeout is reached                        |
| SIGXFSZ (25) | exit(153) + core | exit(1) or exit(11) | sent when max filesize is reached                   |
|--------------+------------------+---------------------+-----------------------------------------------------|



Output Design Goals
-------------------

The rationale for the output described in this document is to have a
uniform way to represent the solutions for different problems related to
ASP.  Output must be easily sent to other programs and designed such
that the grep tool can efficiently get the (main) solution(s) without
major detour.  For this purpose, we designed a line-oriented output
format similar to cookie-jar or record-jar style (see also
http://www.catb.org/esr/writings/taoup/html/ch05s02.html).  The idea
here is that starting from the ANSWER delimiter, we get the content (and
possibly the costs) of a solution using a _fixed_ line offset from this
delimiter.  This corresponds to the -A option to grep and friends.

Important design goals are:

1) delimiters in the output streams are all written in uppercase and are
   single words without whitespace.  In the actual output, delimiters
   must start in the first column.  A delimiter must not be a substring
   of another delimiter;

2) both answer sets and query substitutions are represented as program
   facts such that they can be shipped without processing them to a
   possible next program in a solving pipeline;

3) all output must be streamable, e.g., answer set solvers may dump
   intermediate (non-optimal) solutions for an optimization problem.  In
   this case, they should produce output that corresponds to exit code
   10, but without terminating the process.  If the final optimum is
   eventually found, they can then terminate with exit code 30 and print
   the corresponding output sequence;

4) comments start with the % sign.  They are not allowed to appear
   within an output sequence out_i1, ..., out_ij.  They may appear
   before or after a complete sequence has been printed.

We currently have the following delimiters:

|--------------+--------------------------------------------------------|
| Delimiter    | Meaning                                                |
|--------------+--------------------------------------------------------|
| ANSWER       | Solution found, next line(s) contains answer (+ costs) |
|--------------+--------------------------------------------------------|
| COST         | The cost of the solution in the previous line          |
|--------------+--------------------------------------------------------|
| INCONSISTENT | Program is inconsistent                                |
|--------------+--------------------------------------------------------|
| UNKNOWN      | No solution has been found yet                         |
|--------------+--------------------------------------------------------|
| OPTIMUM      | The solutions given before contain one or more optima  |
|--------------+--------------------------------------------------------|
| %            | The rest of the line is a non-interpreted comment      |
|--------------+--------------------------------------------------------|

NB: a possible "binary" format similar to lparse could be envisaged.
Ground query answers are represented as the facts yes. and no.; again,
pipelining is imperative.  Query substitutions are special: here we
represent the substitutions for a query Q as facts.

The output lines described below---each separated with a newline---must
be present back to back.  That is, out_i must precede out_j for i < j,
and no other output on stdout may appear between the two of them; see
(4) above.  It is not allowed to print newlines or % within an output
line; quoted strings may appear in an answer set, but they are only
allowed to have escaped character such as \\n or \%.

In the Line columns of the tables below, the rows out_1, out_4, and
out_i1 (i = 1,...,m) must _start_ (i.e., at text column 0) with the
shown uppercase string, but may have other (context-dependent) output
following the string until the output ends with a newline.  The line
named out_3 must _start_ with the string COST and followed by a space
and the cost representation of the answer set.  Again, there may be
context-dependent output after this sequence.


Legenda
-------

n/a: not applicable

Run interrupted? : grounder/solver terminates before the given
                   computational problem has been fully computed (e.g.,
                   reception of a signal like SIGINT, SIGKILL, SIGSEGV,
                   or when the machine resources like maximum runtime,
                   memory, or file size is exhausted)

EC    : program exit code
out_i : output line i of an output sequence
out_ij: output line j of the i-th output sequence

A, A_i: answer set of a program
T     : collection of substitutions satisfying a query

Then, facts(A) gives fact representation of an answer set A, i.e., for A
= {a_1, ..., a_n}, facts(A) is

a_1. ... a_n.

Likewise for facts(T), which gives for the collection of substituions T
= {t_1, ..., t_n} the facts

_(t1). ... _(tn).

(FIXME: how to represent facts of T: _ is not an appropriate symbol for
a predicate.)

The function opt(P,A) gives a space-separated sequence of cost@level
pairs which represent the costs at the respective level of an answer set
A w.r.t. program P:

c1@l1 c2@l2 ...

The grounding output ground(P) of a program P is not specified, here
either lparse or textual output may appear in consecutive output lines.


Computing the Grounding of Program P
------------------------------------

|------------------+--------------------------+-----+-----------|
| Run interrupted? | P syntactically correct? |  EC | Output    |
|------------------+--------------------------+-----+-----------|
| no               | yes                      |   0 | ground(P) |
|------------------+--------------------------+-----+-----------|
| no               | no                       | 128 | n/a       |
|------------------+--------------------------+-----+-----------|
|------------------+--------------------------+-----+-----------|
| yes              | yes                      |   1 | n/a       |
|------------------+--------------------------+-----+-----------|


Search Problem for Program P
----------------------------

|------------------+---------------+---------+----+-------+--------------|
| Run interrupted? | P consistent? | answer? | EC | Line  | Output       |
|------------------+---------------+---------+----+-------+--------------|
| no               | yes           | A       | 10 | out_1 | ANSWER       |
|                  |               |         |    | out_2 | facts(A)     |
|------------------+---------------+---------+----+-------+--------------|
| no               | no            | n/a     | 20 | out_1 | INCONSISTENT |
|------------------+---------------+---------+----+-------+--------------|
|------------------+---------------+---------+----+-------+--------------|
| yes              | n/a           | n/a     |  1 | out_1 | UNKNOWN      |
|------------------+---------------+---------+----+-------+--------------|

(This is just a special case of n=1 enumeration problem.)


Answer Set n-Enumeration Problem for Program P
----------------------------------------------

|------------------+---------------+-----+--------------------+----+--------+--------------|
| Run interrupted? | P consistent? | n   | answers?           | EC | Line   | Output       |
|------------------+---------------+-----+--------------------+----+--------+--------------|
| no               | yes           | > 0 | A_1, ..., A_n      | 10 | out_11 | ANSWER       |
|                  |               |     |                    |    | out_12 | facts(A_1)   |
|                  |               |     |                    |    |        | ...          |
|                  |               |     |                    |    | out_n1 | ANSWER       |
|                  |               |     |                    |    | out_n2 | facts(A_n)   |
|------------------+---------------+-----+--------------------+----+--------+--------------|
| no               | no            | ≥ 0 | n/a                | 20 | out_11 | INCONSISTENT |
|------------------+---------------+-----+--------------------+----+--------+--------------|
| no               | yes           | ≥ 0 | A_1, ..., A_m      | 30 | out_11 | ANSWER       |
|                  |               |     | (n > 0: 0 < m < n) |    | out_12 | facts(A_1)   |
|                  |               |     | (n = 0: m > n)     |    |        | ...          |
|                  |               |     |                    |    | out_m1 | ANSWER       |
|                  |               |     |                    |    | out_m2 | facts(A_m)   |
|------------------+---------------+-----+--------------------+----+--------+--------------|
|------------------+---------------+-----+--------------------+----+--------+--------------|
| yes              | n/a           | ≥ 0 | n/a                |  1 | out_11 | UNKNOWN      |
|------------------+---------------+-----+--------------------+----+--------+--------------|
| yes              | yes           | ≥ 0 | A_1, ..., A_k, ... | 11 | out_11 | ANSWER       |
|                  |               |     | (n > 0: k < n)     |    | out_12 | facts(A_1)   |
|                  |               |     | (n = 0: k > n)     |    |        | ...          |
|                  |               |     |                    |    | out_k1 | ANSWER       |
|                  |               |     |                    |    | out_k2 | facts(A_k)   |
|------------------+---------------+-----+--------------------+----+--------+--------------|



Optimization n-c-Enumeration Problem for Program P
------------------------------------------------

|------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
| Run interrupted? | P consistent? | n   | c   | answers?           | all optima <= c? | EC | Line   | Output          |
|------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
| no               | yes           | > 0 | ≥ 0 | A_1, ..., A_n      | n/a              | 10 | out_11 | ANSWER          |
|                  |               |     |     |                    |                  |    | out_12 | facts(A_1)      |
|                  |               |     |     |                    |                  |    | out_13 | COST opt(P,A_1) |
|                  |               |     |     |                    |                  |    |        | ...             |
|                  |               |     |     |                    |                  |    | out_n1 | ANSWER          |
|                  |               |     |     |                    |                  |    | out_n2 | facts(A_k)      |
|                  |               |     |     |                    |                  |    | out_n3 | COST opt(P,A_k) |
|------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
| no               | no            | ≥ 0 | ≥ 0 | n/a                | n/a              | 20 | out_11 | INCONSISTENT    |
|------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
| no               | yes           | ≥ 0 | ≥ 0 | A_1, ..., A_m      | yes              | 30 | out_11 | ANSWER          |
|                  |               |     |     | (n > 0: 0 < m < n) |                  |    | out_12 | facts(A_1)      |
|                  |               |     |     | (n = 0: m > n)     |                  |    | out_13 | COST opt(P,A_1) |
|                  |               |     |     |                    |                  |    |        | ...             |
|                  |               |     |     |                    |                  |    | out_m1 | ANSWER          |
|                  |               |     |     |                    |                  |    | out_m2 | facts(A_m)      |
|                  |               |     |     |                    |                  |    | out_m3 | COST opt(P,A_m) |
|                  |               |     |     |                    |                  |    | out_m4 | OPTIMUM         |
|------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
|------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
| yes              | n/a           | ≥ 0 | ≥ 0 | n/a                | n/a              |  1 | out_11 | UNKNOWN         |
|------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
| yes              | yes           | ≥ 0 | ≥ 0 | A_1, ..., A_k, ... | n/a              | 11 | out_11 | ANSWER          |
|                  |               |     |     | (n > 0: k < n)     |                  |    | out_12 | facts(A_1)      |
|                  |               |     |     | (n = 0: k > n)     |                  |    | out_13 | COST opt(P,A_1) |
|                  |               |     |     |                    |                  |    |        | ...             |
|                  |               |     |     |                    |                  |    | out_k1 | ANSWER          |
|                  |               |     |     |                    |                  |    | out_k2 | facts(A_k)      |
|                  |               |     |     |                    |                  |    | out_k3 | COST opt(P,A_k) |
|------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|


Ground Query Q w.r.t. Program P
-------------------------------

|------------------+--------+----+-------+---------|
| Run interrupted? | P |= Q | EC | Line  | Output  |
|------------------+--------+----+-------+---------|
| no               | true   | 10 | out_1 | ANSWER  |
|                  |        |    | out_2 | yes.    |
|------------------+--------+----+-------+---------|
| no               | false  | 20 | out_1 | ANSWER  |
|                  |        |    | out_2 | no.     |
|------------------+--------+----+-------+---------|
|------------------+--------+----+-------+---------|
| yes              | n/a    |  1 | out_1 | UNKNOWN |
|------------------+--------+----+-------+---------|

Brave and cautious query answering gives the same output, the user
decides upfront which query service is being instantiated.


Nonground Query Q w.r.t. Program P
----------------------------------

|------------------+---------------+--------+----+-------+--------------|
| Run interrupted? | P consistent? | P |= Q | EC | Line  | out_1        |
|------------------+---------------+--------+----+-------+--------------|
| no               | yes           | T      | 10 | out_1 | ANSWER       |
|                  |               |        |    | out_2 | facts(T)     |
|------------------+---------------+--------+----+-------+--------------|
| no               | no            | n/a    | 20 | out_1 | INCONSISTENT |
|------------------+---------------+--------+----+-------+--------------|
|------------------+---------------+--------+----+-------+--------------|
| yes              | n/a           | n/a    |  1 | out_1 | UNKNOWN      |
|------------------+---------------+--------+----+-------+--------------|

If T=0, facts(T) in out_2 corresponds to a newline ('\n').


Enumerating Brave or Cautious Consequences of a Program P
---------------------------------------------------------

|------------------+---------------+-----+----------------------------+----+--------+----------------|
| Run interrupted? | P consistent? | n   | Enumerated consequences    | EC | Line   | Output         |
|------------------+---------------+-----+----------------------------+----+--------+----------------|
| no               | yes           | > 0 | Cn_1(P), ..., Cn_n(P)      | 10 | out_11 | ANSWER         |
|                  |               |     |                            |    | out_12 | facts(Cn_1(P)) |
|                  |               |     |                            |    |        | ...            |
|                  |               |     |                            |    | out_n1 | ANSWER         |
|                  |               |     |                            |    | out_n2 | facts(Cn_n(P)) |
|------------------+---------------+-----+----------------------------+----+--------+----------------|
| no               | no            | ≥ 0 | n/a                        | 20 | out_11 | INCONSISTENT   |
|------------------+---------------+-----+----------------------------+----+--------+----------------|
| no               | yes           | ≥ 0 | Cn_1(P), ..., Cn_m(P)      | 30 | out_11 | ANSWER         |
|                  |               |     | (n > 0: 0 < m < n)         |    | out_12 | facts(Cn_1(P)) |
|                  |               |     | (n = 0: m > n)             |    |        | ...            |
|                  |               |     |                            |    | out_m1 | ANSWER         |
|                  |               |     |                            |    | out_m2 | facts(Cn_m(P)) |
|------------------+---------------+-----+----------------------------+----+--------+----------------|
|------------------+---------------+-----+----------------------------+----+--------+----------------|
| yes              | n/a           | ≥ 0 | n/a                        |  1 | out_11 | UNKNOWN        |
|------------------+---------------+-----+----------------------------+----+--------+----------------|
| yes              | yes           | ≥ 0 | Cn_1(P), ..., Cn_k(P), ... | 11 | out_11 | ANSWER         |
|                  |               |     | (n > 0: k < n)             |    | out_12 | facts(Cn_1(P)) |
|                  |               |     | (n = 0: k > n)             |    |        | ...            |
|                  |               |     |                            |    | out_k1 | ANSWER         |
|                  |               |     |                            |    | out_k2 | facts(Cn_k(P)) |
|------------------+---------------+-----+----------------------------+----+--------+----------------|