v1: change in invariant analysis to make it deterministic (TODO: needs to be removed/replaced before merging because it is too expensive)
v2: change in balance check that fixes the issue for the example task but leads to changes in five domains (plus domain variations)
v3: fixed bug in v2. We now get the same invariants as before (while bug is fixed) but overall slower (which in particularly bites us in trucks-strips where the invariant analysis runs out of time).
v4: resolves an old todo to use itertools instead of the function cartesian_product in tools.py -> same invariants
v5: explicit representation of invariant parameters through variables "?@vi" -> same invariants, up to 22 seconds more time for finding invariants
v6: attempt to reduce computation time by restructuring the code -> mild improvements
v7: like v6 but removed logging (slowing down everything since v3) and added an output to verify that some code never fires. -> faster than v4 and bug fixed :-)
v8: changed naming and structure in constraints.py to make meaning clearer. -> faster than v1 and bug of course still fixed.
v9: different way to prevent equivalence of variable and constant, changed naming and structure in invariants.py to make code clearer.
v10: reverted change from v1 (invariant synthesis again not deterministic)
v11: represent invariant parameters with numbers -> dominates base version time- and memory-wise.
v12: incorporates changes from code review and closes a gap that does not occur in the benchmarks

The cases where the output differs are due to the known non-determinism of the invariant synthesis and not related to the changes in this issue.

Resolved and merged. :-)

The changes from after the code review look good to me, and the experimental results as well. I did not look into the cases where the output sas differed, but I assume you did :).

I incorporated all feedback and if the code passes the code review it is ready to merge from my side.

Experiments (comparing to unmodified Fast Downward): https://ai.dmi.unibas.ch/_experiments/ai/downward/issue1133/data/issue1133-v12-vs-base-eval/

I now represent the invariant parameters with numbers, so the memory overhead is gone and we have a version that is better than the base version, both in terms of memory and time. In particular on the domains where the invariance analysis takes long, we save about a third of the time. :-)

The code is now ready for reviewing.

Pull request: https://github.com/aibasel/downward/pull/212
Experiment (v11, compared against base): https://ai.dmi.unibas.ch/_experiments/ai/downward/issue1133/data/issue1133-v11-eval/issue1133-v11-23499409976f669b036ef162b2835832f01d2fb2-issue1133-v11-compare.html

This issue ended up in a major revision of the code for finding invariants (the old one was uncommented and quite incomprehensible).
It probably does not help a lot to look at the diff because I renamed and restructured basically everything (and added lots of comments).

Besides fixing the bug, I also took care of some potential runtime bottlenecks, so the invariance synthesis is now faster (in particular on the grounded tasks).
For clarity reasons, I also made a change how the invariants are internally represented. Previously, the invariant parameters did not have names (but we referred to them by numbers). The current code uses variable names of the form "?@v0" for the purpose. This change improved the code readability but made it slightly slower and increased the memory consumption.
Maybe it is worth to reconsider this decision (but using an easier-to-understand representation based on numbers)

I still already create a pull request for the current version in case someone wants to have a look:

Pull request: https://github.com/aibasel/downward/pull/212
Experiment (v10, compared against base version): https://ai.dmi.unibas.ch/_experiments/ai/downward/issue1133/data/issue1133-v10-eval/issue1133-v10-23499409976f669b036ef162b2835832f01d2fb2-issue1133-v10-compare.html

The translator output did not change (differences are caused by the existing non-determinism of the invariance analysis).

I unbundled what was previously combined in the "renamings" in the code (and did not really correspond to the renamings in the pseudo code). This leads to a restructuring of the entire construction of the equality system.

I am not sure whether the current code is already worth looking at because I expect significant further changes. It definitively is far from being ready for a pull request.

If you are nevertheless interested, you can find it at https://github.com/roeger/downward/tree/issue1133.

The way I understood the previous code, this "limiting the scope of the invariant" already happened (perhaps no intentionally) by adding constraints of the form (?v0 = a2) to the constraint system. I guess this was not enough. I'd be interested in understanding this better (both the problem with the current code and your fix). 

Also, what do you mean with "we need to adapt the entire balance check"? From what I wrote in the first message here, I thought the only method that doesn't do what it is supposed to is "unbalanced_renamings()", i.e., only the part that checks in which of a given set of renamings a given delete effect does not balance a given add effect.

Is there a pull request with the changes?

The balance check did not really cover this situation, neither does the pseudo code in the translator paper: it requires to minimally rename the action parameters so that the invariant covers the add effect. Since the constants in the add effect cannot be controlled by the action parameters, this is not possible in this situation. Instead we would have to rename the parameters of the invariant. This corresponds to limiting the scope of the invariant for the balance check to the situation where the corresponding invariant parameter is fixed to the constant. Thus, we need to adapt the entire balance check.

Initial experiments are running.

An example instance to reproduce the bug is attached. The translator reports the instance as trivially unsolvable. However, the planner finds a solution if we run the translator without invariant synthesis.

Consider a task with constants a1, a2, b1, b2 and a single predicate p(a, b).

The invariant synthesis considers a candidate p(a, [b]), i.e., "for a fixed a there is at most one b, such that p(a,b) is true". The candidate should be rejected for the following action but isn't.

board(?a: a)
Precondition:
  Atom p(?a, b1)
Effects:
  ~p(?a, b1)
  if p(a2, b1) then p(a2, b2)

We already discussed this for some time on Discord and think that the reason that should trigger is that the add effect (if p(a2, b1) then p(a2, b2)) is not balanced by the only delete effect (~p(?a, b1)). While the effect is balanced in board(a2), it is not balanced in board(a1).

When checking for balance in invariants.py (operator_unbalanced(...)), all add effects relevant to the candidate are checked (add_effect_unbalanced(...)) in our case there is only one. To check the add effect, we first compute a minimal renaming to make the add effect cover the invariant (there is only one minimal renaming in our case). We then check if any delete effect (only one in our case) balances the add effect with minimal renaming. This happens in the function unbalanced_renamings() that is supposed to return the renamings from the minimal renamings where the delete effect does not balance the add effect. In our case, we would expect it to return one element, but it return an empty list.

The function unbalanced_renamings() is called as expected for
  * the delete effect "~p(?a, b1)",
  * the add effect "if p(a2, b1) then p(a2, b2)",
  * the candidate p(?v0, ?v1) with counted variables V = {?v0}, and
  * a minimal renaming given as the following constraint system:
    ASS:  ((?v0 = a2))

All of these inputs look correct up until here and we would now expect that the function returns an element as still_unbalanced. But it doesn't.