Done and merged.

I looked at the code, looks good to me.

Alternatively, we could also explore to introduce a goal action (that needs to be handled by the search component as a post-processing of the plan).

I implemented the fix that enforces a binary encoding of all atoms that occur negatively in the goal. This resolves the issue and I would consider it a better solution than introducing an axiom (which would not be supported by many heuristics).

The experiments don't look critical to me. All differences in output.sas are in the few domains where we always experience non-determinism.

Experiments: https://ai.dmi.unibas.ch/_experiments/ai/downward/issue1127/data/issue1127-v1-eval/issue1127-v1-23499409976f669b036ef162b2835832f01d2fb2-issue1127-v1-compare.html
Pull request: https://github.com/aibasel/downward/pull/217

Getting back to the general limitation (not the specific example task), one way to support negative literals in the goal would be to force them to be encoded with binary variables. Then it is easy to express them with "the other" value. Since we never ran into the assertion with our benchmark tasks, this should not harm their encoding.

In the code, we call translate_strips_conditions_aux twice, first with the full mutex information, afterwards with the actual FDR encoding. From the first call, we currently only use the information whether there are conflicting conditions, so it seems a bit excessive to me to continue the computation beyond this decision.

Getting back to the bug: I think it is clear that we want to drop an implied negative condition from the goal (otherwise we run into an assertion). The question is whether we want to drop them in general (avoiding a transformation into a DNF condition, which ultimately leads to several copies of actions or conditional effects for the different conjunctions).

The actually used variables don't use this mutex group, so we would need to drop negated effects already in the earlier call of the auxiliary method (where we hand in full mutex information).

This bug relates to a limitation of the translator wrt. negative goals.

If the goal requires (not (P x y)) and (P x y) is encoded by a FDR variable with 5 possible values, we conceptually would need to replace the negative goal with a disjunction over the other 4 values of this variable. Since a normalized goal may not contain a disjunction, we instead would need to add another axiom, something we don't want to do that late in the process (we basically are too lazy because negative goals are rare). In the restricted case where the variable only has 2 possible values, we just add the corresponding other value, which is the reason why the assertion does not fail if the invariance analysis is switched off.

In this particular example, we have a specific situation which we might want to address. The example is a simple gripper task with goal (and (not (carry ball4 left)) (at ball4 roomb)). We have a FDR variable for [Atom at(ball4, ?X), Atom carry(ball4, ?X)].
So (at ball4 roomb) already implies (not (carry ball4 left)) and we should simply drop the negative goal.
The right place for this adaptation would be in translate_strips_conditions_aux.py in the part starting at line 97.

The translator may throw an exception in certain cases when a negated goal is part of a finite-domain 
variable with more than two values.

https://github.com/aibasel/downward/blob/main/src/translate/translate.py#L490

Attached you find a gripper example, where this happens. It does not happen if you disable mutex and 
finite domain variable generation.

(originally reported by David Speck)