PR for this issue: https://github.com/aibasel/downward/pull/308

I ran some experiments with the fix (https://ai.dmi.unibas.ch/_experiments/ai/downward/issue1240/data/) and on the benchmarks from the downward-benchmarks repository the performance seems to stay roughly the same. Also, the output of the translator stays the same which we expected since none of the benchmarks fall into the special case that needed treatment.

I also ran experiments on more benchmarks with axioms (https://github.com/roeger/axiom_benchmarks). Same as with the downward-benchmarks the performance stays roughly the same here.

Unexpectedly, the translator output changes on four domains (cats-tseitin-{var1,var2}, elevator-tseitin-{var1,var2}) with our fix although they do not fall into the special case. In their output.sas files the names of some variables introduced by the translator change. The reason is that with the fix we change in which order eliminate_universal_quantifiers iterates through the conditions of a task (actions -> axioms -> goal previously, actions -> goal -> axioms now). This leads to different variable numberings on those domains.
There is a way to implement the fix such that the order does not change but this would duplicate some code and make the corresponding code fragment less clear to understand. Because of this we decided to stick with the current version of the fix.

An expected difference in the translator output comes from the spanning-tree domain (which falls into the special case). With the fix the axioms in output.sas remain stratifiable.

Given those experiment results I think the PR (https://github.com/aibasel/downward/pull/308) is ready for a review now.

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