Implement Naive Grounding

[miquelramirez]

From the e-mail

Naive grounding: no es ideal, pero no siempre podremos usar el ASP grounder (e.g. when functions available, etc.). Un punto interesante es si queremos "forzar" el uso del ASP grounder when possible, e.g. by reformulating the problem into STRIPS without functions (just for the purpose of feeding it into the ASP module), and then extracting the info from there.

Tasks:

• [x] Define output format
• [x] Implement state variable calculation procedure
• [x] Implement action grounding procedure
• [x] Implement universal quantifier elimination
• [x] Implement constraint grounding procedure
• [ ] Implement HDF5 writer for storing groundings of symbols

[miquelramirez]

For the output format I suggest we use HDF5 to store the groundings etc.

[miquelramirez]

First pass on "calculation" of state variables, see commit -- https://github.com/aig-upf/tarski/commit/c7cf3c8997054a15d3cd300ed314c59c283116bc

[miquelramirez]

Managed to push forward a bit the implementation of the naive method for action grounding, the grounding itself still lives in the tests, since I am not very sure where it would be best to have it right now. Some observations that have occurred to me while doing this:

• Simplification of grounded representations really needs to happen on the backend. The reason for this is that I cannot see why Tarski needs to assume that the planning backend will be considering certain symbols to have an static extension -- other than built-ins and tautologies (i.e. if we have x = x, that's top regardless of the model chosen by the user, and if we have (very complex existentially quantified formula) conjoined with (x=x), we know we can replace the whole thing by top regardless of the model. Does this pose a design problem that needs to be solved?

• Now I see as well that we need to implement the transformation "Elimination of Universal Quantification" in order to be able to ground correctly both action effects and constraints. Is it necessary to transform every formula into Prenex? Should we transform into CNF too as a pre-processing step?

• Regarding the notion of primary and secondary variables... it is now clear to me that we do not need to make any differentiation... other than grounding formulas
  1. \exists y, loc(y) = x,
  2. \exists y, loc(x) = y and
  3. \exists x,y ax + by < 0 correctly requires different strategies. The first one would need to be come a disjunction loc(a) =x \lor loc(b) = x \lor loc(c) = x. The second one would require doing nothing too special. And the third one would require to create specific state variables (this case corresponds with the secondary variables from Patrik's framework). Can you think of more cases like this @gfrances ?

[gfrances]

Simplification of grounded representations really needs to happen on the backend. The reason for this is that I cannot see why Tarski needs to assume that the planning backend will be considering certain symbols to have an static extension

Having a layer for that in the backend sounds reasonable; one question, though: in a standard STRIPS domain, what obstacle do you see to Tarski assuming that a symbol whose denotation is never modified by any action is static (say, connected in Sokoban), and simplifying accordingly (say, removing a ground action with precondition connected(p1, p34) when that atoms doesn't hold)? That's already done by the ASP reachability check.

Now I see as well that we need to implement the transformation "Elimination of Universal Quantification" in order to be able to ground correctly both action effects and constraints. Is it

I'm ok with having these transformations as optional preprocessing steps, if they are necessary. We can even easily have a "dependency graph" of transformations, that tells us e.g. that if you want to apply fancy transformation "Y", the prerequisite is that the problem is in form "X", which can be achieved by transformations "Z" and "A" (sorry, ran out of letters :-)). i.e. a modular / pluggable architecture.

the second one would require doing nothing too special. And the third one would require to create specific state variables (this case corresponds with the secondary variables from Patrik's framework) The second one is a tautology, indeed. The point with the third one is: why do we need then to create a new state variable? What state variable would that be¿?

[miquelramirez]

see to Tarski assuming that a symbol whose denotation is never modified by any action

"In a standard STRIPS domain" - that is a safe assumption. When you have procedural terms, atoms and effects, it is not. Does Tarski need to know when the planning problem being modelled is "standard STRIPS? If so, we then need to think to have something like the "requirements" keywords from PDDL.

i.e. a modular / pluggable architecture.

Yes, that sounds like the way to go.

The point with the third one is: why do we need then to create a new state variable? What state variable would that be¿?

If the state is to be a formula, then all the variables featured in every subformula/subterm should "state variables", right? How do you handle this stuff with \existential-FSTRIPS?

[gfrances]

"In a standard STRIPS domain" - that is a safe assumption. When you have procedural terms, atoms and effects, it is not. Why not? Any procedural symbol is, by definition, static: it's denotation will never change, and it's given by some deterministic C++ function. Of course, another matter is that perhaps the python frontend is not able to execute that code, and thus cannot reason about denotations involving external symbols. But this is not because the symbol might be fluent, but simply because the frontend cannot execute the C++ procedure (at least not in the current architecture). I see now that perhaps this is what you meant?

If the state is to be a formula, then all the variables featured in every subformula/subterm should "state variables", right? How do you handle this stuff with \existential-FSTRIPS?

But again, are we talking about classical FSTRIPS? In that case, the state is not a formula, is an interpretation, which can assign a truth value to \exists x,y ax + by < 0 with no need for any extra variable...? Or am I missing something?

[gfrances]

@miquelramirez, what's the status of the idea of the "HDF5 writer"? Should we file that as a separate "enhancement" issue and close this one? Sounds like a potentially interesting idea, although I'm not sure I'd prioritize that at least until we have some clear use case, i.e. some domain where storing / retrieving the groundings is what kills the performance (perhaps we already have that? excuse my ignorance. Although thinking about it, if we have that, not sure that clingo would ever be able to tackle it??)

[miquelramirez]

This was an old idea, no longer relevant.