search

alpha-asp / Alpha

A lazy-grounding Answer-Set Programming system
BSD 2-Clause "Simplified" License
58 stars 10 forks source link

Investigate Rule Decomposition #70

Open lorenzleutgeb opened 6 years ago

lorenzleutgeb commented 6 years ago

Basic idea, informally:

There is lpopt which implements this kind of rewriting.

What can we learn from that to make Alpha better? Would it make sense to implement this rewriting into Alpha's lazy grounding?

AntoniusW commented 6 years ago

This is a very good observation! Indeed, the authors of lpopt suggested this already some months ago and I also think that this could be a very good optimisation.

There is one potential obstacle, however, which might make Alpha slower when using rule decomposition. Decomposing a rule might introduce many rules that project variables, i.e., where there are more variables in the body than in the head. Such rules easily trigger a problem with must-be-true after reaching a fixpoint in the solving, which currently requires exponential time in order to undo the guess that causes the presence of must-be-true. Therefore, I saw this must-be-true issue as a stopper to such optimisations, but there might very well be many cases where the optimisation does not cause problems. One has to check that experimentally. Additionally, there is a new collaboration that might develop into solving the must-be-true issue.

From what I understood, the lpopt tool does some rather complex rewriting and it might be quite involved. So far, I assumed it were easier to just pipe the input ASP program through lpopt. If you are interested in working on this issue, I am happy to establish a collaboration with the authors of lpopt.

lorenzleutgeb commented 6 years ago

OK, it seems we agree. I expected some additional challenges with MBT, but this was just a gut feeling. Good to have that confirmation.

As a first step, we might evaluate the effects of lpopt preprocessing on Alpha as suggested. Then we might actually re-implement (a subset of) lpopt re-writings and evaluate again (and probably only then involve the authors of lpopt).

AntoniusW commented 6 years ago

We can run an initial evaluation of preprocessing with lpopt on our own but should keep the authors of lpopt in the loop early on, because I actually promised them to keep them informed as soon as I/we have any results. :-)

votacom commented 6 years ago

Just weighing in (I developed the current version of lpopt).

Thanks for your interest in rule decomposition and considering supporting it in Alpha. Rule decomposition has also already been successfully adapted in the grounder I-DLV.

If you'll eventually decide to get it on, I'd be glad to help with any questions that arise.

AntoniusW commented 6 years ago

Thank you for that offer!

Now we just need a volunteer to advance this issue. :-)

lorenzleutgeb commented 6 years ago

@AntoniusW, am I right that the issue that you refer to in https://github.com/alpha-asp/Alpha/issues/70#issuecomment-340288324 has been resolved by #130 / Exploiting Justifications for Lazy Grounding of Answer Set Programs?

AntoniusW commented 6 years ago

Hi @lorenzleutgeb, yes the issue has been resolved in principle by #130 and this issue here is no longer blocked.