The current translator handles disjunctions in preconditions, effect conditions, and axiom bodies by converting formulas to disjunctive normal form (DNF) and creating one instance for each disjunct. For example, a precondition containing a disjunction results in multiple copies of the same operator. Since the DNF transformation can be exponential in the size of the formula, this approach may lead to an exponential runtime and task size.

In this issue, we plan to add an optional translator option that introduces auxiliary derived variables to decompose disjunctive formulas instead of expanding them into DNF. The resulting translation has polynomial size but requires evaluating the auxiliary variables for each state using axioms.

Experiments: https://ai.dmi.unibas.ch/_experiments/ai/downward/issue1222/

The first experiment (v1_translate) shows that the output.sas files are identical for option 1 (dnf, the default) and the current main branch. The other options only produce different output.sas files when disjunctions and/or existential quantifiers are present.

The second experiment runs astar-blind (v1_optimal) and lama-first (v1_satisficing) on the full benchmark set (the optimal and satisficing suites, plus some additional domains with complicated formulas for stress testing). These experiments show that, overall, the default (dnf) approach is often the best choice for the standard domains with complicated formulas (maybe they are a bit cherry-picked). However, for more complex constructs, the other options provide a clear benefit by being able to ground and solve problems that the current default cannot.

Additionally, we see that introducing more axioms results in higher memory usage. For folding-sat23-adl, this is particularly apparent when running astar-blind, where we are unable to solve two instances because we run out of memory. This issue can be addressed by not storing the values of derived predicates in the state registry, since they are fully determined by the primary variables anyway. However, this will hopefully be addressed in another issue.

So, to me, the experiments show that the default behavior remains unchanged, while we now have two suitable alternatives for handling more complicated formulas.

We identified the handling of existential quantifiers as an interesting design question.

In Fast Downward, existential quantifiers are handled by introducing additional parameters for actions and axioms. For the goal, however, this is not possible (without a post processing of the plan), which is why we current replace complex goals with a derived predicate defined by a single axiom by default.

For the axiom-based decomposition of complex formulas, one can leave existential quantifiers as they are, but for the goal we also need to handle them differently. For now, we aim at three different strategies:

- Option 1 (current and future default): Replace complex goals with a derived predicate defined by a single axiom and naively convert all conditions to DNF.
- Option 2: Replace complex goals with a derived predicate defined by a single axiom and decompose all disjunctions using derived predicates.
- Option 3: Decompose every disjunction and existential quantifier in action conditions and the goal, while decomposing only disjunctions in axiom bodies.

Overall, these three options already illustrate that there is a spectrum regarding how aggressively one wants to decompose formulas and move logic into axioms. At one extreme, every condition could be represented by a single derived predicate. For now, we decided on these three options for the following reasons:

- Option 1 tries to avoid axioms, as they are not supported by many planner components.
- Option 2 decomposes complex formulas and thus avoids the exponential behavior of Option 1. However, it may introduce (more) axioms.
- Option 3 generally introduces the largest number of axioms, but it has the nice property that it does not produce multiple operator instances for the same original operator (as Option 1&2 may do). This can be particularly helpful for reasoning about the plan space, for example in plan counting and enumeration.

Finally, Malte mentioned that moving the existential quantifiers to axioms (Option 3) can lead to a smaller space of choices for the join tree decomposition with a negative effect on grounding.

PR: https://github.com/aibasel/downward/pull/297