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.
|