Computing globally minimal answers

It is common that given a query there are multiple answers. Sometimes, we are interested in the minimal solution(s). In a ground answer, the set of collected constraints can be discarded as they are ground and must be satisfiable. Therefore, the set of collected abducibles can represent the whole ground answer.

Let $\widehat{\Delta}$ be the set of all ground answers as sets of abducibles. An answer $\Delta_{i} \in \widehat{\Delta}$ is minimal if and only if there is no $\Delta_{j} \in \widehat{\Delta}$ such that $\Delta_{j} \subset \Delta_{i}$.

The abductive system provides a special querying predicate eval(+ListOfGoals, -ListOfAbducibles) for computing globally minimal answers, which can succeed only if the following two conditions are satisfied:

• the computation of all (possibly non-ground) answers terminates;
• all the non-ground answers can be grounded by grounding the finite domain variables appearing in the answers.

Note that another difference between query/2 and eval/2 is that the second argument of eval/2 is a list of abducibles, instead of a tuple as for query/2. In addition, the abductive system also provides a predicate eval(+ListOfGoals, +Time, -ListOfAbducibles), which will succeeds if and only if eval(+ListOfGoals, -ListOfAbducibles) succeeds within the given Time (in milliseconds).