I merged and pushed.

I did one more change pointed out by Malte. I think we can merge this now.

Thanks. I updated the pull request. The tests also finished without issue.

Thanks, Florian! I left some bitbucket comments.

I added issue878 for the additional information on equivalent facts.

I created a pull request for this:
https://bitbucket.org/FlorianPommerening/downward-issues/pull-requests/54

I started a small experiments that translates the first 4-5 tasks of all domains
with the new and old translator and checks that the output stays the same and
that the new assertion doesn't trigger. It also translates the tasks with the
full encoding to check that no assertion triggers. So far everything looks good.

Sounds good. (We discussed this in the sprint meeting this morning.)

The problem is in line 604 in translate.py: if an atom is represented by several
variable-value pairs, we add them all to the mutex group, basically saying that
the atom is mutex with itself.

Since with the full encoding all mutex information is already covered by the
variable encoding, the obvious solution would be not to generate mutex
information if using the full encoding.

The information that two variable-value pairs represent the same fact gets lost
in the translator output. This might be useful for some purposes (e.g. potential
heuristics). I would not make such a change as part of this issue but maybe add
another low-priority issue to not loose the idea.

I'm not sure if I have tested this thoroughly enough, but it seems to me that
the planner emits nonsensical mutex information when using the "--full-encoding"
option. Running

./translate.py --full-encoding
~/downward/benchmarks/blocks/{domain.pddl,probBLOCKS-4-0.pddl}

gives me the attached output.sas file. For example, the fact "(on a b)" is
represented with the assignments "var0=1" and "var7=2", but one of the mutex
groups claims that (0, 1) and (7, 2) are mutex, which makes no sense. It is
possible that the mutex code was never tested for the full encoding and
internally assumes that every variable only has one internal representation.

Generally speaking, it is not clear how to best represent mutex information for
the full encoding. Partially quoting from an email of mine:

For the full encoding, I think there are cases where this sort of information
cannot be represented in less than quadratic space in the form of mutex groups
(because there can be quadratically many interactions of this form), and for the
larger planning benchmarks, quadratic runtime or space can be prohibitive. There
exist benchmark tasks with more than 100000 facts, so mutex pair information
represented in a flat way can consist of more that 10^10 pairs, which means that
we would need something like 10^11 bytes to write it down, or 100 GB, just to
represent the mutexes. This is of course something we cannot afford.

In the partial encoding, it is possible to work around this by storing larger
sets of mutex groups, which can always be done in linear time in the size of the
internal representation. In the full encoding, I don't think this is possible.
One would need a different form of compact representation.