See meta-issue: issue924.

We want to simplify the translator output format by only allowing binary derived
variables whose default value is always false, and only allowing axioms setting
a derived variable to true. "Negated axioms" should instead be computed in the
search component when needed (for example in cg/landmarks/relaxation heuristics).

See msg8204 of issue862 for an overview of how the axiom code currently works.
(May become out of date while we're working on the axiom code further.)
(the axiom code was heavily reworked with issue453)

Check for references to "issue454" in the code, specifically axiom_rules.py and
sas_tasks.py. (Best look for references to issue454 in the whole codebase.)

Further TODOs/plans moved from issue862:
- Try moving the computation of axiom layers earlier, having everything related
  to negated axiom rules at the end. Then simplify the layer computation code
  to take into account that it no longer has to deal with negated heads, and
  enable the test that verifies the layering condition properly, removing all
  the hacks that are currently there because of the negated rules.
  Add assertions that there are no negated heads. Then rerun the experiments.
- Open an issue for the bug with compute_necessary_axiom_literals
  (see msg8204). (this was resolved as part of issue453)
- Make a plan for further steps for the axiom code. See the various notes etc.
  in msg8204.

I looked into the different expansions for psr. It had nothing to do with the transformation to multi-valued variables, but with the fact that axioms are simplified after computing dependencies between derived variables. The simplification can remove cyclic dependencies, which influence how we compute negated axioms. If a derived variable is needed negatively but has cyclic dependencies, we overapproximate the negation with a default true (i.e. we introduce one axiom that sets the variable to false without any conditions). Since the task transformation computes the dependencies after simplification, it thus can exactly compute the negation in more cases now.

For example, in psr-large/p02-s46-n3-l5-f50.pddl we have the following two axioms before simplification:
(unsafe sd2 side2)
PRE: Atom closed(sd2)
EFF: Atom unsafe(sd2, side2)

(unsafe sd2 side2)
PRE: Atom closed(sd2)
PRE: Atom unsafe(sd3, side1)
EFF: Atom unsafe(sd2, side2)

The second one is unnecessary and thus simplified away, but it introduces a dependency between unsafe(sd2, side2) and unsafe(sd3, side1), which eventually leads to a cycle involving those two. (The latter variable doesn't even occur in output.sas anymore since it is irrelevant.)

I implemented the computation of negated axioms as a task transformation that heuristics apply if they can make use of negated axioms. (These heuristics are all relaxation heuristics, the landmark sum heuristic and the cg and cea heuristics which depend on the domain transition graph.)

Here is the pull request:
https://github.com/aibasel/downward/pull/220

And here the experimental results:
https://ai.dmi.unibas.ch/_experiments/ai/downward/issue454/data/issue454-v3-eval/issue454-v3-issue454-base-issue454-v3-compare.html


In general the results are encouraging in the sense that not much changes. With hmax and cea we even gain 1 task. But as usually happens, the landmark configurations are a bit worse :). lama-first looses 2 tasks and rhw (that is just eager greedy search with landmark sum over the rhw graph) recognizes one less task as unsolvable.

There are slight differences in the number of expansions. For blind and goalcount (which should not be influenced by negated axioms) this happens in philosophers and trucks; I think we know that these domains can have nondeterministic translator output (for trucks I know for sure). The other configurations except for rhw also have different expansions in psr-large and psr middle; for all but lama-first it is less.
My best guess is that this happens because the translator computed the negated axioms still on the pddl task; that it is just encoded the negated conditions as "Negated Literal", and the transformation to multi-valued variables happens later. The task transformation on the other hand needs to negate a multi-valued variable. I do this by replacing "¬v=d" with "\/_{d' \in dom(v), d' != d) v=d'".
For example, assume we have two variables v0 and v1 with dom(v0) = dom(v1) = {0,1,2}, and two axioms for some fact f: a1 with conditions (v0=0 and v1=1) and a2 with conditions (v0=1 and v1=1). The negation of these conditions in the translator is simply (¬v0=0 or ¬v1=1) for a1 and (¬v0=1 or ¬v1=1) for a2. The task transformation on the other hand turns this into (v0=1 or v0=2 or v1=1 or v1=2) for a1 and (v0=0 or v0=2 or v1=0 or v1=2). When multiplying this out it will ignore combinations that set different values to the same var, so the multiplied out version (removing dominated conjunctions) will be (v0=1 and v1=0) or (v0=2) or (v1=1 and v0=0) or (v1=2).

If for the experiments you need a list of domains with axioms:

- airport-adl
- assembly
- miconic-fulladl 
- openstacks
- openstacks-opt08-adl
- openstacks-sat08-adl 
- optical-telegraphs
- philosophers
- psr-large
- psr-middle
- trucks

While working on issue453, we changed the handling of axioms in the translator to
set the default value of derived variables to false. We can now continue to clean
up the translator output format and move the computation of negated axioms rules
into the search component. I updated the summary accordingly.

I added the remaining TODOs from the resolved issue862 to the summary because
they fit this issue better.

Add a pointer to msg8204 to the summary.

BTW, I'm no longer convinced that changing this would only affect a few parts of
the code. It looks like at least most of our relaxation heuristics (h^FF, h^add,
h^max) make use of the axioms provided by the code, and ripping out the negated
axiom versions can have a strong negative impact on them.

I don't mean this as an excuse to leave this issue unfixed, of course. But it
does mean we need to tread a bit carefully. In particular, we should make sure
not to ruin performance in cases without cyclic dependencies, which includes all
cases where derived variables are currently artificially introduced by the
translator.

Made the summary more comprehensive.

I'm reclassifying this as a bug because the negated axiom rules mean that we can
currently have axiom rules with heads (v=0) and (v=1) for the same variable. (At
least I think that this can happen.)

This is not necessarily a problem due to the way the axioms are actually
constructed, but it does not agree with how we specified the layering condition
in the AIJ paper on the translator and elsewhere. So at the very least, we
should make the semantics and the behaviour of the translator clear.

One reasonable place where this could be documented (in addition to the code
itself) is http://www.fast-downward.org/TranslatorOutputFormat, in particular
sections "Variables section" and "Axiom section" and section "Evaluation axioms"
at the end.

The proposed fix for issue862 interacts with this issue.

I've added code comments to axiom_rules.py which explain the interaction. All
relevant comments mention the keyword "issue454", so searching for this keyword
in axiom_rules.py while working on this issue should be enough to find all of
them. I've added a reminder of this to the summary.

Note to self: when fixing this, search the code (in particular the translator)
for references to issue454. The work-in-progress code for issue533 has a code
comment related to this issue.

We currently generate "negated forms" of axiom rules in certain cases. This can
be very expensive, is only used in few contexts, and is apparently currently
buggy (see issue453).

This issue is about getting rid of these negated-form axioms. The most difficult
part in this is probably detecting all the places where they are implicitly used
(e.g. in relevance analysis?). We should also evaluate the performance impact on
planner configurations that make use of these negated axiom rules (such as the
CG heuristic and possibly some of the landmark generators) and possibly
reintroduce them locally for planner configurations that use them.