Attachment 'aspoutput.txt'
Download 1 Answer Set Solver Output
2 ========================
3
4 Thomas Krennwallner <tkren at kr dot tuwien dot ac dot at>
5 February 1, 2013
6
7 The purpose of this document is to standardize the exit codes and the
8 output of grounders and solvers for different computational problems
9 associated with answer set programs. The tables below represent what
10 should appear on stdout in the out_i and out_ij lines, and what
11 should be the respective exit code of the solver in each case. Solvers
12 may write warnings, statistics, and debug information on stdout using
13 comment lines.
14
15
16 Exit Code Bit Encoding
17 ----------------------
18
19 Each exit code represents a possibly successful run of a
20 solver/grounder: based on the exit status, the end user should be able
21 to answer decision problems without parsing the output, or decide
22 whether something went wrong or no solution could be found.
23
24 Exit codes must fit within the lowest 8 bits of an integer. In order to
25 be backward-compatible with SAT/QBF solvers, we use the status values 10
26 and 20 to encode satisfiable and unsatisfiable instances, respectively.
27 This gives the following bit patterns for satisfiable and unsatisfiable
28 runs: 00001010 resp. 00010100. Furthermore, SAT/QBF solvers may exit
29 without a known solution (e.g., when they have hit the time/memory
30 limit), but their exit status do not agree with these kind of runs.
31
32 As ASP solvers usually implement many different computational problems,
33 three exit codes are not enough to give us all information on the exit
34 status of a solver. For this reason, we use the following bit scheme to
35 encode the status of a ground/solver run.
36
37 |-------+-------+-------+---------+-------+---------+-------+-------|
38 | bit 7 | bit 6 | bit 5 | bit 4 | bit 3 | bit 2 | bit 1 | bit 0 |
39 |-------+-------+-------+---------+-------+---------+-------+-------|
40 | NORUN | RES1 | RES2 | EXHAUST | SAT | EXHAUST | SAT | INT |
41 |-------+-------+-------+---------+-------+---------+-------+-------|
42
43 The top row of the table denote the position of the bit in a char, and
44 the bottom row shows the name of the bit.
45
46 The highest bit NORUN is used to signal whenever the grounder/solver did
47 not start the computation. There could be several reasons, most likely
48 whenever the input instance is syntactically unsupported, there is a
49 syntax error, or a command line argument is not known or conflicts with
50 another one. Hence, exit code 128 must be used whenever the
51 grounder/solver process quits without starting the computation. The
52 NORUN bit is mutually exclusive with all other bits.
53
54 The lowest bit INT encodes that the grounder/solver was being terminated
55 by the environment (i.e., received a signal) without completing the
56 computation to the given problem. This bit must be set in the exit code
57 of runs where the grounder/solver gets a signal from the environment, or
58 when computational ressources like time or memory are exhausted. Thus,
59 exit status 1 (or 11) is used in runs, where no (complete) solution is
60 known or where the grounding had been interrupted. When the solver has
61 been interrupted during an enumeration task and after enumerating some
62 models, the exit code will have this bit set to true; those runs
63 correspond to exit code 11.
64
65 The other bits---RES1, RES2, EXHAUST, and SAT---are used for solver runs
66 that found some solutions to a given problem. Grounders do not touch
67 these bits, thus successful grounding runs have exit code 0, which is
68 important for grounding/solving pipelines. Setting the SAT bit encodes
69 that the solver found at least one solution. The EXHAUST flag is used
70 to signal that the solver exhaustively went through the search space.
71 For instance, inconsistent instances have bit EXHAUST and bit SAT set to
72 1 and 0, resp.: this corresponds to an exit status with value 20. Bits
73 RES1 and RES2 are not specified here, they are reserved for future use.
74 Both of them must be set to 0 whenever INT is 0. For instance,
75 implementors may use them to encode further status information for
76 interrupted runs. The specified exit codes in this document can be
77 always retrieved from such exit codes with a bitmask of 0x9f.
78
79 We currently have the following exit codes:
80
81 |-----------+--------------------------------------------------------------------------------------|
82 | Exit code | Meaning |
83 |-----------+--------------------------------------------------------------------------------------|
84 | 1 | Run interrupted: No solution has been found so far |
85 |-----------+--------------------------------------------------------------------------------------|
86 | 10 | Program is consistent / some consequences exist / one optimum found / query is true |
87 |-----------+--------------------------------------------------------------------------------------|
88 | 11 | Run interrupted: Program is consistent / some consequences exist |
89 |-----------+--------------------------------------------------------------------------------------|
90 | 20 | Program is inconsistent / query is false |
91 |-----------+--------------------------------------------------------------------------------------|
92 | 30 | Program is consistent, all possible solutions/consequences enumerated / optima found |
93 |-----------+--------------------------------------------------------------------------------------|
94 | 128 | Syntax error / command line arguments error |
95 |-----------+--------------------------------------------------------------------------------------|
96
97 The following table summarises the expected behaviour of a solver when
98 interrupted by one of the following (standard) termination signals:
99
100 |-------------+------------------+---------------------+-------------------|
101 | Reason | Default action | Expected action | Description |
102 |-------------+------------------+---------------------+-------------------|
103 | SIGHUP (1) | exit(129) | exit(1) or exit(11) | kill -HUP |
104 | SIGINT (2) | exit(130) | exit(1) or exit(11) | Ctrl-C |
105 | SIGQUIT (3) | exit(131) + core | exit(1) or exit(11) | Ctrl-\ |
106 |-------------+------------------+---------------------+-------------------|
107
108 Further signals are relevant in the context of the ASP Competition 2013.
109 Here, different signals encode the reason for solver termination.
110
111 |--------------+------------------+---------------------+-----------------------------------------------------|
112 | Reason | Default action | Expected action | Description |
113 |--------------+------------------+---------------------+-----------------------------------------------------|
114 | SIGKILL (9) | exit(137) | cannot be changed | sent when process(es) continue to run after timeout |
115 | SIGSEGV (11) | exit(139) | exit(1) or exit(11) | sent when memout is reached, or programming error |
116 | SIGTERM (15) | exit(143) | exit(1) or exit(11) | sent at most 10 secs after timeout |
117 | SIGXCPU (24) | exit(152) + core | exit(1) or exit(11) | sent when timeout is reached |
118 | SIGXFSZ (25) | exit(153) + core | exit(1) or exit(11) | sent when max filesize is reached |
119 |--------------+------------------+---------------------+-----------------------------------------------------|
120
121
122
123 Output Design Goals
124 -------------------
125
126 The rationale for the output described in this document is to have a
127 uniform way to represent the solutions for different problems related to
128 ASP. Output must be easily sent to other programs and designed such
129 that the grep tool can efficiently get the (main) solution(s) without
130 major detour. For this purpose, we designed a line-oriented output
131 format similar to cookie-jar or record-jar style (see also
132 http://www.catb.org/esr/writings/taoup/html/ch05s02.html). The idea
133 here is that starting from the ANSWER delimiter, we get the content (and
134 possibly the costs) of a solution using a _fixed_ line offset from this
135 delimiter. This corresponds to the -A option to grep and friends.
136
137 Important design goals are:
138
139 1) delimiters in the output streams are all written in uppercase and are
140 single words without whitespace. In the actual output, delimiters
141 must start in the first column. A delimiter must not be a substring
142 of another delimiter;
143
144 2) both answer sets and query substitutions are represented as program
145 facts such that they can be shipped without processing them to a
146 possible next program in a solving pipeline;
147
148 3) all output must be streamable, e.g., answer set solvers may dump
149 intermediate (non-optimal) solutions for an optimization problem. In
150 this case, they should produce output that corresponds to exit code
151 10, but without terminating the process. If the final optimum is
152 eventually found, they can then terminate with exit code 30 and print
153 the corresponding output sequence;
154
155 4) comments start with the % sign. They are not allowed to appear
156 within an output sequence out_i1, ..., out_ij. They may appear
157 before or after a complete sequence has been printed.
158
159 We currently have the following delimiters:
160
161 |--------------+--------------------------------------------------------|
162 | Delimiter | Meaning |
163 |--------------+--------------------------------------------------------|
164 | ANSWER | Solution found, next line(s) contains answer (+ costs) |
165 |--------------+--------------------------------------------------------|
166 | COST | The cost of the solution in the previous line |
167 |--------------+--------------------------------------------------------|
168 | INCONSISTENT | Program is inconsistent |
169 |--------------+--------------------------------------------------------|
170 | UNKNOWN | No solution has been found yet |
171 |--------------+--------------------------------------------------------|
172 | OPTIMUM | The solutions given before contain one or more optima |
173 |--------------+--------------------------------------------------------|
174 | % | The rest of the line is a non-interpreted comment |
175 |--------------+--------------------------------------------------------|
176
177 NB: a possible "binary" format similar to lparse could be envisaged.
178 Ground query answers are represented as the facts yes. and no.; again,
179 pipelining is imperative. Query substitutions are special: here we
180 represent the substitutions for a query Q as facts.
181
182 The output lines described below---each separated with a newline---must
183 be present back to back. That is, out_i must precede out_j for i < j,
184 and no other output on stdout may appear between the two of them; see
185 (4) above. It is not allowed to print newlines or % within an output
186 line; quoted strings may appear in an answer set, but they are only
187 allowed to have escaped character such as \\n or \%.
188
189 In the Line columns of the tables below, the rows out_1, out_4, and
190 out_i1 (i = 1,...,m) must _start_ (i.e., at text column 0) with the
191 shown uppercase string, but may have other (context-dependent) output
192 following the string until the output ends with a newline. The line
193 named out_3 must _start_ with the string COST and followed by a space
194 and the cost representation of the answer set. Again, there may be
195 context-dependent output after this sequence.
196
197
198 Legenda
199 -------
200
201 n/a: not applicable
202
203 Run interrupted? : grounder/solver terminates before the given
204 computational problem has been fully computed (e.g.,
205 reception of a signal like SIGINT, SIGKILL, SIGSEGV,
206 or when the machine resources like maximum runtime,
207 memory, or file size is exhausted)
208
209 EC : program exit code
210 out_i : output line i of an output sequence
211 out_ij: output line j of the i-th output sequence
212
213 A, A_i: answer set of a program
214 T : collection of substitutions satisfying a query
215
216 Then, facts(A) gives fact representation of an answer set A, i.e., for A
217 = {a_1, ..., a_n}, facts(A) is
218
219 a_1. ... a_n.
220
221 Likewise for facts(T), which gives for the collection of substituions T
222 = {t_1, ..., t_n} the facts
223
224 _(t1). ... _(tn).
225
226 (FIXME: how to represent facts of T: _ is not an appropriate symbol for
227 a predicate.)
228
229 The function opt(P,A) gives a space-separated sequence of cost@level
230 pairs which represent the costs at the respective level of an answer set
231 A w.r.t. program P:
232
233 c1@l1 c2@l2 ...
234
235 The grounding output ground(P) of a program P is not specified, here
236 either lparse or textual output may appear in consecutive output lines.
237
238
239 Computing the Grounding of Program P
240 ------------------------------------
241
242 |------------------+--------------------------+-----+-----------|
243 | Run interrupted? | P syntactically correct? | EC | Output |
244 |------------------+--------------------------+-----+-----------|
245 | no | yes | 0 | ground(P) |
246 |------------------+--------------------------+-----+-----------|
247 | no | no | 128 | n/a |
248 |------------------+--------------------------+-----+-----------|
249 |------------------+--------------------------+-----+-----------|
250 | yes | yes | 1 | n/a |
251 |------------------+--------------------------+-----+-----------|
252
253
254 Search Problem for Program P
255 ----------------------------
256
257 |------------------+---------------+---------+----+-------+--------------|
258 | Run interrupted? | P consistent? | answer? | EC | Line | Output |
259 |------------------+---------------+---------+----+-------+--------------|
260 | no | yes | A | 10 | out_1 | ANSWER |
261 | | | | | out_2 | facts(A) |
262 |------------------+---------------+---------+----+-------+--------------|
263 | no | no | n/a | 20 | out_1 | INCONSISTENT |
264 |------------------+---------------+---------+----+-------+--------------|
265 |------------------+---------------+---------+----+-------+--------------|
266 | yes | n/a | n/a | 1 | out_1 | UNKNOWN |
267 |------------------+---------------+---------+----+-------+--------------|
268
269 (This is just a special case of n=1 enumeration problem.)
270
271
272 Answer Set n-Enumeration Problem for Program P
273 ----------------------------------------------
274
275 |------------------+---------------+-----+--------------------+----+--------+--------------|
276 | Run interrupted? | P consistent? | n | answers? | EC | Line | Output |
277 |------------------+---------------+-----+--------------------+----+--------+--------------|
278 | no | yes | > 0 | A_1, ..., A_n | 10 | out_11 | ANSWER |
279 | | | | | | out_12 | facts(A_1) |
280 | | | | | | | ... |
281 | | | | | | out_n1 | ANSWER |
282 | | | | | | out_n2 | facts(A_n) |
283 |------------------+---------------+-----+--------------------+----+--------+--------------|
284 | no | no | ≥ 0 | n/a | 20 | out_11 | INCONSISTENT |
285 |------------------+---------------+-----+--------------------+----+--------+--------------|
286 | no | yes | ≥ 0 | A_1, ..., A_m | 30 | out_11 | ANSWER |
287 | | | | (n > 0: 0 < m < n) | | out_12 | facts(A_1) |
288 | | | | (n = 0: m > n) | | | ... |
289 | | | | | | out_m1 | ANSWER |
290 | | | | | | out_m2 | facts(A_m) |
291 |------------------+---------------+-----+--------------------+----+--------+--------------|
292 |------------------+---------------+-----+--------------------+----+--------+--------------|
293 | yes | n/a | ≥ 0 | n/a | 1 | out_11 | UNKNOWN |
294 |------------------+---------------+-----+--------------------+----+--------+--------------|
295 | yes | yes | ≥ 0 | A_1, ..., A_k, ... | 11 | out_11 | ANSWER |
296 | | | | (n > 0: k < n) | | out_12 | facts(A_1) |
297 | | | | (n = 0: k > n) | | | ... |
298 | | | | | | out_k1 | ANSWER |
299 | | | | | | out_k2 | facts(A_k) |
300 |------------------+---------------+-----+--------------------+----+--------+--------------|
301
302
303
304 Optimization n-c-Enumeration Problem for Program P
305 ------------------------------------------------
306
307 |------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
308 | Run interrupted? | P consistent? | n | c | answers? | all optima <= c? | EC | Line | Output |
309 |------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
310 | no | yes | > 0 | ≥ 0 | A_1, ..., A_n | n/a | 10 | out_11 | ANSWER |
311 | | | | | | | | out_12 | facts(A_1) |
312 | | | | | | | | out_13 | COST opt(P,A_1) |
313 | | | | | | | | | ... |
314 | | | | | | | | out_n1 | ANSWER |
315 | | | | | | | | out_n2 | facts(A_k) |
316 | | | | | | | | out_n3 | COST opt(P,A_k) |
317 |------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
318 | no | no | ≥ 0 | ≥ 0 | n/a | n/a | 20 | out_11 | INCONSISTENT |
319 |------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
320 | no | yes | ≥ 0 | ≥ 0 | A_1, ..., A_m | yes | 30 | out_11 | ANSWER |
321 | | | | | (n > 0: 0 < m < n) | | | out_12 | facts(A_1) |
322 | | | | | (n = 0: m > n) | | | out_13 | COST opt(P,A_1) |
323 | | | | | | | | | ... |
324 | | | | | | | | out_m1 | ANSWER |
325 | | | | | | | | out_m2 | facts(A_m) |
326 | | | | | | | | out_m3 | COST opt(P,A_m) |
327 | | | | | | | | out_m4 | OPTIMUM |
328 |------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
329 |------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
330 | yes | n/a | ≥ 0 | ≥ 0 | n/a | n/a | 1 | out_11 | UNKNOWN |
331 |------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
332 | yes | yes | ≥ 0 | ≥ 0 | A_1, ..., A_k, ... | n/a | 11 | out_11 | ANSWER |
333 | | | | | (n > 0: k < n) | | | out_12 | facts(A_1) |
334 | | | | | (n = 0: k > n) | | | out_13 | COST opt(P,A_1) |
335 | | | | | | | | | ... |
336 | | | | | | | | out_k1 | ANSWER |
337 | | | | | | | | out_k2 | facts(A_k) |
338 | | | | | | | | out_k3 | COST opt(P,A_k) |
339 |------------------+---------------+-----+-----+--------------------+------------------+----+--------+-----------------|
340
341
342 Ground Query Q w.r.t. Program P
343 -------------------------------
344
345 |------------------+--------+----+-------+---------|
346 | Run interrupted? | P |= Q | EC | Line | Output |
347 |------------------+--------+----+-------+---------|
348 | no | true | 10 | out_1 | ANSWER |
349 | | | | out_2 | yes. |
350 |------------------+--------+----+-------+---------|
351 | no | false | 20 | out_1 | ANSWER |
352 | | | | out_2 | no. |
353 |------------------+--------+----+-------+---------|
354 |------------------+--------+----+-------+---------|
355 | yes | n/a | 1 | out_1 | UNKNOWN |
356 |------------------+--------+----+-------+---------|
357
358 Brave and cautious query answering gives the same output, the user
359 decides upfront which query service is being instantiated.
360
361
362 Nonground Query Q w.r.t. Program P
363 ----------------------------------
364
365 |------------------+---------------+--------+----+-------+--------------|
366 | Run interrupted? | P consistent? | P |= Q | EC | Line | out_1 |
367 |------------------+---------------+--------+----+-------+--------------|
368 | no | yes | T | 10 | out_1 | ANSWER |
369 | | | | | out_2 | facts(T) |
370 |------------------+---------------+--------+----+-------+--------------|
371 | no | no | n/a | 20 | out_1 | INCONSISTENT |
372 |------------------+---------------+--------+----+-------+--------------|
373 |------------------+---------------+--------+----+-------+--------------|
374 | yes | n/a | n/a | 1 | out_1 | UNKNOWN |
375 |------------------+---------------+--------+----+-------+--------------|
376
377 If T=0, facts(T) in out_2 corresponds to a newline ('\n').
378
379
380 Enumerating Brave or Cautious Consequences of a Program P
381 ---------------------------------------------------------
382
383 |------------------+---------------+-----+----------------------------+----+--------+----------------|
384 | Run interrupted? | P consistent? | n | Enumerated consequences | EC | Line | Output |
385 |------------------+---------------+-----+----------------------------+----+--------+----------------|
386 | no | yes | > 0 | Cn_1(P), ..., Cn_n(P) | 10 | out_11 | ANSWER |
387 | | | | | | out_12 | facts(Cn_1(P)) |
388 | | | | | | | ... |
389 | | | | | | out_n1 | ANSWER |
390 | | | | | | out_n2 | facts(Cn_n(P)) |
391 |------------------+---------------+-----+----------------------------+----+--------+----------------|
392 | no | no | ≥ 0 | n/a | 20 | out_11 | INCONSISTENT |
393 |------------------+---------------+-----+----------------------------+----+--------+----------------|
394 | no | yes | ≥ 0 | Cn_1(P), ..., Cn_m(P) | 30 | out_11 | ANSWER |
395 | | | | (n > 0: 0 < m < n) | | out_12 | facts(Cn_1(P)) |
396 | | | | (n = 0: m > n) | | | ... |
397 | | | | | | out_m1 | ANSWER |
398 | | | | | | out_m2 | facts(Cn_m(P)) |
399 |------------------+---------------+-----+----------------------------+----+--------+----------------|
400 |------------------+---------------+-----+----------------------------+----+--------+----------------|
401 | yes | n/a | ≥ 0 | n/a | 1 | out_11 | UNKNOWN |
402 |------------------+---------------+-----+----------------------------+----+--------+----------------|
403 | yes | yes | ≥ 0 | Cn_1(P), ..., Cn_k(P), ... | 11 | out_11 | ANSWER |
404 | | | | (n > 0: k < n) | | out_12 | facts(Cn_1(P)) |
405 | | | | (n = 0: k > n) | | | ... |
406 | | | | | | out_k1 | ANSWER |
407 | | | | | | out_k2 | facts(Cn_k(P)) |
408 |------------------+---------------+-----+----------------------------+----+--------+----------------|
Attached Files
You are not allowed to attach a file to this page.