Clingo - Progression error/warning

Question

I'm running the solver on a planning and between the various answer sets i get what I think is a warning (as it does not termiate the execution) saying the following:

Progression : [2;8] (Error: 3)
Progression : [3;8] (Error: 1.66667)
Progression : [4;8] (Error: 1)
Progression : [5;8] (Error: 0.6)
Progression : [6;8] (Error: 0.333333)
Progression : [7;8] (Error: 0.142857)

I can't find any reference to that warnings so I hope someone knows what they mean.

Answer 1

These lines give valuable information about the current state of the optimization: in your example, the solver has found a solution of cost 8 and not yet proved that the solution is optimal, but it is on the way to prove it: it has proved that the cost is at least 2, 3, 4, ..., 7. So if you abort the solver after the last line, you have a guarantee that the solution you found is either optimal or 1 away from optimum.

This information can help you to make comprimises between optimality and solver time. Often you are fine in applications if you have suboptimal results that are close enough to the optimum.

Answer 2

A quick search in the clasp source https://github.com/potassco/clasp/blob/master/src/clasp_output.cpp revealed that method TextOutput::printUnsat is responsible for these messages.

The comment in the base class shows for Output::printUnsat:

//! Called on unsat - may print new info.

Specifically, TextOutput::printUnsat comment is

//! Prints the given lower bound and upper bounds that are known to be optimal.