For axioms that mention their head predicate, possibly recursively, in their body under the scope of a universal quantifier the normalization of the translator makes the set of axioms unstratifiable.
The normalization eliminates universal quantifiers by replacing <forall(vars, phi)> with <not(not-all-phi)>, where <not-all-phi> is a new axiom and is defined as <not(forall(vars,phi))> (translated to NNF). If phi mentions the head predicate, possibly recursively via other derived predicates, then the introduced negation requires the axiom to be in a different stratum than itself which is of course impossible.
The spanning-tree domain (https://github.com/roeger/axiom_benchmarks/tree/master/spanning-tree) is an example for this. Its axioms are stratifiable but Fast Downward crashes on its tasks and says that the axioms are unstratifiable.
Gabi and I started implementing a fix for this where universal quantifiers in axioms of this particular form are eliminated differently. The idea is to replace <forall(vars, phi)> by a conjunction where each conjunct is phi with vars replaced by objects (of fitting types).
This partial grounding will increase the size of the affected axioms but cannot be fully avoided (in our ICAPS 2026 paper we show that without task-specific information the compilation to Datalog is impossible).
|