R10: Metasp

https://arxiv.org/pdf/1107.5742.pdf Links to an external site.

Note: We aren't the target audience for this paper. In this Applied ASP class, we just want to pick up technology and use it for real-world stuff. The papers we read are often trying to reach the audience who is making more ASP tools rather than using them. Unfortunately, these papers are often the only written reference for these ideas while the tricks and practices for doing application work are only traded verbally or in private email. It's okay if 70% of the material goes over (er, around?) your head. It's for someone else.

Gist:

- Disjunctive ASP is more expressive than normal ASP, but it's extremely hard to use directly.

- Familiar #minimize statements already defined a preference ordering between answer sets, and this higher complexity stuff is often targeted about modeling preferences anyway.

- Let's hijack the #minimize statement to do more stuff.

- Writing an entirely new ASP system would be wasteful, so we cleverly reduce the one we want to implement to something that can be decided by the one we already have.

- We apply that esoteric "saturation" trick so you don't have to.

- Reification turns a grounded program into a bunch of facts. From there, we can use mostly familiar syntax in ASP to reason about slightly different semantics of the original program.

- We made reification a standard feature of Gringo so you can make other stuff wit hit.

- As an example application, we did a biology thing.

- Final note: The programs emerging from the use of our metasp tool will be the first useful test of solvers to test \Sigma_2^P-hard problems.

Historical Note

At this point in history, even though the semantics of disjunction were nailed down in the 90s, nobody yet had a really exciting use for disjunction that couldn't be more directly expressed with choice rules -- completely sidestepping the extra complexity / extra expressiveness that comes from that weird subset minimality definition. The saturation trick is was the gateway to modeling anything reducible to 2QBF, a much more popular problem (analogous to SAT, which is really 1QBF). Even in 2017, perhaps 10 people in the world can confidently use the saturation trick directly (including me). Meanwhile, the meta-interpreter approach offered a chance to sweep the theoretical mess under the rug and jump directly on to exciting applications. We cover the extra expressiveness of disjunctive ASP in a textbook on game content generation because it is so easy to hide the scary formulation now.