DeMaCS-UNICAL / I-DLV

The new intelligent grounder of the logic-based Artificial Intelligence system DLV
https://github.com/DeMaCS-UNICAL/I-DLV/wiki
22 stars 0 forks source link

Recursion through a sum aggregate #3

Closed jbomanson closed 3 years ago

jbomanson commented 3 years ago

Hi!

I have a program with recursion through an aggregate. Running idlv on the program yields an unexpected ground program with some rules missing. I would expect it to either give the correct output or to show an error message in case such recursion is not supported.

This also appears to be the underlying cause of unexpected behaviour of Dlv2 reported in the publication https://www.aaai.org/ojs/index.php/AAAI/article/view/4119 . (See "We report no numbers for Dlv2 here, because ..."). I apologize for reporting this with such a delay.

Contents of program.asp:

bound(1).
{s(1)}.
{s(2)}.
bound(X1) :- sum(X), X1 = X+1.
sum(K) :- K<=#sum{X:s(X)}, bound(K).

Outpupt of bin/idlv_1.1.5_linux_x86-64 program.asp --t:

bound(1).
d(1).
d(2).
{s(1)}.
{s(2)}.
sum(1):-1<=#sum{1:s(1);2:s(2)}.
bound(2):-sum(1).

Output of gringo program.asp --text:

bound(1).
d(1).
d(2).
{s(1)}.
{s(2)}.
sum(1):-1<=#sum{1:s(1);2:s(2)}.
bound(2):-sum(1).
sum(2):-bound(2),2<=#sum{1:s(1);2:s(2)}.
bound(3):-sum(2).
sum(3):-bound(3),3<=#sum{1:s(1);2:s(2)}.
bound(4):-sum(3).
jessicazangari commented 3 years ago

Hi,

thanks a lot for your feedback. We confirm this seems to be a bug, we are going to fix it and update executables. Concerning DLV2, please note that it does not support recursive aggregates as it adheres to the ASP-Core-2 standard. We started supporting recursion through aggregates starting from version 1.1.5 of I-DLV, whereas WASP and DLV2 do not support it yet. However, one can still use I-DLV 1.1.5 in combination with clingo in clasp mode.

jbomanson commented 3 years ago

Cool :thumbsup: That is interesting to know--thanks for the clarification.

jessicazangari commented 3 years ago

Hi,

we fixed the bug and just updated executables of version 1.1.5. Actually, the issue was not on recursive aggregates because in your example the predicate s/1 is not recursive but it occurred in case of recursive rules with aggregates. I'm going to close the issue. We will fix it also in DLV2, but in the meantime we suggest you to use I-DLV 1.1.5 in combination with CLASP/WASP. Thanks again for your feedback and for the interest in our system!