[issue1222] Add translator option for representing disjunctive formulas using derived variables - #297
[issue1222] Add translator option for representing disjunctive formulas using derived variables#297speckdavid wants to merge 8 commits into
Conversation
2244678 to
3dd46df
Compare
| def eliminate_disjunctive_conditions(task): | ||
| condition_strategy = get_options().condition_normalization_strategy | ||
| if condition_strategy == "dnf": | ||
| substitute_complicated_goal(task) |
There was a problem hiding this comment.
I am not convinced that this should be encapsulated in something called eliminate_disjunctive_conditions. It's not only about this. For example, it would also replace an existential condition with a (derived) atom.
Your strategy would not transform such a goal and it seems to be handled fine by a later stage of the normalization. But in this case, we probably also should restrict substitute_complicated_goal to disjunctive formulas. Are there other corner cases of goal formulas that need to be considered?
There was a problem hiding this comment.
Very good point.
We (@SimonDold and I) looked into it again and realized that the existential quantifiers were not handled as expected. In fact, they are also a form of "or" and later in the pipeline pulled out where the variables then are used as parameters. This process is not in the spirit of the axiom_based approach. Furthermore, this is not possible for the goal.
So, we changed the method to not only move disjunctions but also existential quantifiers into axioms.
Accordingly, we renamed eliminate_disjunctive_conditions to simplyfy_conditions because after the process only "simple conditions", i.e., conjuncitons and existential conditions, remain (+ truth values, literals).
There was a problem hiding this comment.
Top-level existential quantifiers of operators and axioms behave the same way semantically as parameters. For axioms, they have exactly the same semantics; for operators, the only difference is whether the parameters are part of the action name or not. Is there a good argument for compiling them into axioms? It potentially means that grounding cannot be as efficient any more because we have a smaller space of choices for the join tree decomposition, and we get axiom-based tasks in what could be a STRIPS/SAS+ tasks.
(For the goal it's different because the goal cannot have parameters.)
Perhaps something we should discuss live?
…n. It is now moved to the axioms as body.
…tentials' condition normalization strategies.
6 participants
The translator has now an option
condition-normalization-strategywhich allows to choice between the following two options.dnf(default): The previous strategy to handle disjunctions in conditions. It produces a dnf and splits the condition. For the goal it may substitute at the highest level using axioms.axioms_based(new): Decompose disjunctive formulas using derived predicates. It replaces each disjunctive subformula with a derived predicate and add a corresponding axiom defining that predicate. The transformation proceeds bottom-up so nested disjunctions are eliminated first.