Issue453

Title Solvable problem reported unsolvable - incorrect computation of derived predicates?
Priority bug Status chatting
Superseder Nosy List augusto, gabi, jendrik, malte, patrik, salome
Assigned To Keywords translator
Optional summary
See meta-issue: issue924.

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

Check for references to "issue453" in the code, specifically axiom_rules.py.

TODOs:

1. Have a translator option that implements the new strategy with the trivial
overapproximation. Make sure that relaxed reachability and relevance analysis
play nicely with this. Make sure that the axiom evaluator in the search code
ignores the fake rules. (In general, to make this work also with the old
behaviour, we can ignore all rules where the head is the default value of the
variable.)

2. Later, we probably want to try more sophisticated things, e.g. don't
overapproximate if there are no cycles.

Created on 2014-08-16.03:28:28 by patrik, last changed by malte.

Summary
See meta-issue: issue924.

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

Check for references to "issue453" in the code, specifically axiom_rules.py.

TODOs:

1. Have a translator option that implements the new strategy with the trivial
overapproximation. Make sure that relaxed reachability and relevance analysis
play nicely with this. Make sure that the axiom evaluator in the search code
ignores the fake rules. (In general, to make this work also with the old
behaviour, we can ignore all rules where the head is the default value of the
variable.)

2. Later, we probably want to try more sophisticated things, e.g. don't
overapproximate if there are no cycles.
Files
File name Uploaded Type Edit Remove
disjunction.pddl patrik, 2014-08-16.03:28:28 application/octet-stream
disjunction2.pddl patrik, 2014-08-16.03:28:49 application/octet-stream
disjunction2.pre patrik, 2014-08-21.03:10:27 application/octet-stream
disjunction2.sas patrik, 2014-08-21.03:10:16 application/octet-stream
disjunction2.soln patrik, 2014-08-16.03:29:03 application/octet-stream
fd-val.cc patrik, 2014-08-16.03:29:55 text/x-c++src
Messages
msg8893 (view) Author: malte Date: 2019-06-12.23:16:19
These rules are not quite complete/correct. For example, the second rule talks
about the effect condition of an operator, but operators don't have effect
conditions; effects do.

It should be something like: If L is necessary and <if cond then L> is a
conditional effect of an operator o (cond may be trivial), then all literals in
pre(o) and cond are necessary.


The last overapproximation rule is probably meant to say that the complement of
L is (overapproximated as) necessary if *L* occurs in any precondition, effect
condition or axiom body; otherwise that rule is identical to the one before.

Note that this overapproximation is a lot weaker than the (buggy, but assuming
that were fixed) overapproximation we currently use; I'm not sure it is
meangingfully different from "everything is relevant". Rather than use this
overapproximation, it is probably a better implementation effort/benefit
trade-off not to compute any notion of "necessary" at all.
msg8882 (view) Author: augusto Date: 2019-06-12.14:47:00
As discussed today, we are refactoring the code for the axiom rules generation
and one issue is the definition of "necessary literals". When computing the
axiom rules to be used, we only use the rules for which the variable in the head
is necessary.

Our definition of 'necessary literal' is:
 - A literal L is necessary if L occurs in the goal
 - If a literal L is necessary and L \in eff(o) of some operator O, then every
literal L' \in pre(o) and L' \in effcond(o) is necessary
 - If a negated literal ~L is necessary and L \in eff(o) of some operator O,
then every literal L' \in effcond(o) is necessary
 - If a literal L is necessary and occurs in the head of some axiom rule A, then
every literal  L' occurring in the body of A is necessary
 - If a negated literal ~L is necessary and L occurs in the head of some axiom
rule A, then every literal L' occurring in the body of A is necessary


However, using these rules, we need to perform a relevance analysis to figure
out which literals are necessary or not.

Another possibility is to use an approximation of the rules in order to avoid
computing the relevance analysis at this point. The approximation of these rules
would be:

 - A literal L is necessary if it occurs in the goal
 - A literal L is necessary if it occurs in any precondition, effect condition,
or body of axiom rules
 - A negated literal ~L is necessary if it occurs in any precondition, effect
condition, or body of axiom rules

This approximation makes things easier for now, but it might hurt performance
significantly. Ideally, we would like to test both definitions of *necessary
literal* to see which one is preferable.
msg8865 (view) Author: salome Date: 2019-06-07.12:00:57
We discussed several options today on how a more sophisticated implementation
should look like. In general, we want to restructure the axiom code to use some
clearer data structures, starting with computing an SCC early on which will be
used to (1) decide for which variables we can safely only keep the negative
axioms, and (2) compute the axiom layers at the end.

For (1), we also want to investigate whether it is even beneficial to delete the
original axioms, since we can only do this for variables which are in its own
SCC. (For all other variables, we can add the sophisticated negative axioms, but
are not allowed to delete the original ones and switch the default value.)

For (2), we want to test whether we should aim for a minimal or maximal amount
of layers.
msg8851 (view) Author: augusto Date: 2019-06-06.16:05:17
Oh, I did not check these issues before.
I will add the ones related to the issue experiments.

Since the grid is full now, I ran a few local tests using the lazy greedy search
with FF and 8GB as memory limit. I call as "normal" the current version of the
axiom rules in the translator and as "overapproximation" rules the one we are
testing. The version using overapproximation of axiom rules solves almost all
problems, while the normal version runs out-of-memory in almost all cases. The
only exception is the "graph domain" where we fail during the computation of the
canonical model. In summary, our method solved all the performance issues of
these domains. In fact, all instances had less than one second of search time
when using the overapproximation. 


More detailed results: (just to keep track of what is related and what is not)
- problems in issue165
  - the clean cup domain runs out of memory very quick using the normal version,
but it is solved very quick (1 second) using the overapproximation;
  - for the blocksworld no clear domain: the small instance (5 blocks) is easily
solved by both versions; while the large one (10 blocks) runs out-of-memory for
our normal version but is solved in less than one second by the
overapproximation version. The same happens for Patrik's
"crash-dummy-domain.pddl" variant of this domain.
   - the graph domain runs out-of-memory while computing/instantiating the
canonical model. Thus, it is not related to the axiom problem.

- problems in issue450
  - citycar domain: computing the canonical model and instantiating the schemas
already uses ~6GB. Using the normal axiom rules, we run out of memory as soon as
we start simplifying the axioms. Using the overapproximation, the axioms still
take a while to generate. In total, the overapproximation generates 1.177.879
axioms. However, FF reports it as unsolvable. Are we sure this instance is
solvable? I ran it with goalcount and the blind heuristic and it also did not
find a solution. If it is solvable, then we have a bug in our code. 
  - mst: runs out of memory using the normal version; solved very quickly using
the overapproximation.

- problems in issue533
  - the instances from this issue did not produce any error in neither version.
msg8849 (view) Author: malte Date: 2019-06-06.15:38:20
These are good points/questions. Perhaps have a brief discussion about this?
More generally, our current collection of issues related to this is a bit of a
mess; it may help to consolidate it a bit.
msg8848 (view) Author: salome Date: 2019-06-06.15:21:31
Thanks Augusto!

To my understanding, the next step would be to only use the trivial
overapproximation when there are cycles containing negative derived literals. I
have however a few questions about implementation details:

1. The best place to look for cycles would be when creating the axiom layer.
However, this happens only after we make the decision to overapproximate or not.
The easiest solution is to simply calculate the dependency graph twice, once in
the beginning when we want to see if cycles exist, and later when creating the
layers. But in msg8204 Malte mentioned that it might be a good idea to compute
the layers much earlier. Plus I think there was also somewhere an argument to
change the layer computation from creating as few layers as possible to create
as many as possible?
My suggestion would be to open a new issue for possible changes to the layer
computation, and for this issue stick with simple solution (unless performance
suffers too much).

2. As Augusto mentioned we currently consider *all* literals necessary when
using the overapproximation. We do this because axioms for unnecessary literals
get discarded. In the normal setting, if a derived variable is only necessary in
its negative form, the "original" axioms get discarded and instead axioms for
its negation get introduced. But since the overapproximation setting only
introduce an overapproximation for the negative form, we would loose information
by discarding the "original" axioms. Would a correct behaviour be to stick with
the computation of necessary literals, but always add both the literal and its
negation?
msg8847 (view) Author: malte Date: 2019-06-06.15:19:09
There are also instances attached to issue165, issue450, issue533 and issue862
that may be related. I think it would make sense to consolidate them in one
place and include them in the issue experiments. (I'm not saying all of these
are related, but all of them may be.)
msg8846 (view) Author: augusto Date: 2019-06-06.15:14:10
I assume that you are talking about the instances posted by Patrik in this issue
and posted by Gabi in issue862, right?
If yes, then both instances are correctly solved when using the
overapproximation (but the one by Patrik is obviously still not correct when not
using it.)
msg8845 (view) Author: malte Date: 2019-06-06.15:00:49
So far, so good!

Can you test the benchmarks that are linked to this issue and the related issues
where our code currently behaves incorrectly, and see if the change fixes the
problem?

I'm reasonably confident we can get performance back up by addressing the issues
with simplification/relevance analysis and by not overapproximating in cases
where the exact negated rules can be computed with reasonable effort.

The only domain where there may be conceptually challenges ahead is PSR, but for
now I'm mildly optimistic.
msg8844 (view) Author: augusto Date: 2019-06-06.14:54:30
The results are in

http://inf.ufrgs.br/~abcorrea/_issues/issue453/issue453-v1.html

(Sorry for the sciCORE error messages. But my module loads seem correct --
assuming that Jendrik's are also correct :-)

I ran the experiments proposed by Malte in msg8235. "normal" indicates the
current method used by Fast Downward, "overapprox" is using the option to
trivially overapproximate axiom rules as described in msg8795. 
I ran an initial experiment to filter out instances where we generated at least
one axiom, thus I am only reporting on those instances where axioms are produced
but, for some reason, I removed airport-adl. I am running a new experiment only
with airport-adl. It ends up that all other domains are the same reported by
Malte in msg8235.

The overapproximation seems to be very harmful in general. It increases the
number of axioms significantly (as expected) but it also makes the heuristic
estimates much worse (check the initial h-values). It is interesting to see that
the causal graph heuristic (cg) is significantly more informed than the
delete-free heuristics in a few domains when using the overapproximation approach.
We also have an instance of psr-large where the translator runs out-of-memory in
our overapproximation, which is very bad since the "normal" version multiplies
out the CNF and still doesn't run out-of-memory. The new approach is, in
general, significantly slower than the "normal" one.
One possible issue with our approach is that we create axioms for every single
literal instead of just using the literals which are necessary (i.e., that
appear in a precondition or in the goal).
msg8819 (view) Author: malte Date: 2019-06-05.19:33:03
As discussed offline: msg8235 lists the axiom-related search plugins that I
think should be tested. I may have missed something when I compiled the list,
but I think it should give us decent enough coverage.
msg8810 (view) Author: augusto Date: 2019-06-05.15:07:29
We finished the implementation of the trivial overapproximation as an option for
the translation. We will run some experiments using the causal graph heuristic,
the delete-relaxation heuristics, and the landmark heuristics to check whether
they work fine with it. I already noticed that the Zhu and Given landmark
factory is not safe when used ADL domains. (We probably should state it more
clearly in the wiki.)

Malte, is there any specific configuration that you want us to test? 
I thought about: context-enhanced additive heuristic, causal graph heuristic, FF
heuristic, LM-count heuristic with RHW landmark factory, blind heuristic, and
some other heuristic which does not rely on axioms (e.g., iPDB). Am I missing
some obvious configuration that we would like to test?
msg8795 (view) Author: malte Date: 2019-06-04.11:11:10
We want to work with two representations for the axioms. Firstly, the "actual"
true representation that is used by the axiom evaluator. Unlike currently, we
want this to be the original unadultered axioms, i.e., not reformulate some of
them from positive to negative and change the default value. All default values
will be the negative literals, all rules will derive a positive literal. Unlike
currently, in this representation we have no explicit representations of under
which conditions we get the negated value, only the implicit one "we get it if
we don't derive the positive one".

For the heuristics, we need to tell them something about the conditions under
which we can get the negative values. Previously, we had the reformulated rules
for this. But we can also use any overapproximation. For now, we will try the
trivial overapproximation where we use "fake rules" of the form "=> not x"
(empty left-hand side) to tell the heuristics "we can get not x unconditionally".

Some parts of the planner need the exact representation, some parts need
explicit rules for the negative values, but can use an overapproximation for now.
msg8790 (view) Author: augusto Date: 2019-06-03.17:06:25
We are back to this issue. We decided to implement the overapproximation, as
explained by Malte in msg8047 but generating these rules for every literal
occurring in some axiom rule. In this way, we can solve the problem caused by
the cyclic dependency of derived predicates, and we do not break the
implementation of the delete-free heuristics nor the causal graph heuristic. I
will create a branch in my repo for this issue.

Besides the modification in axiom_rules.py, we also need to adapt the search
component (axiom.cc) to avoid possible "non-determinism" when evaluating the
axioms with this overapproximation. Basically, whenever two axioms are triggered
with different values for the same derived predicate, we should set the value of
this predicate to its default value.

Another issue is regarding the relevance analysis performed by the translator
after the generation of axiom rules. We must guarantee that no information is
lost due to the overapproximation of the axiom rules.
msg8206 (view) Author: malte Date: 2018-12-08.13:24:43
Add a pointer to msg8204 to the summary.
msg8047 (view) Author: malte Date: 2018-11-04.07:05:43
I've thought about this some more, and I want to write down the outcomes of this
thought process before I forget about it again. What we do with this in order to
fix this issue is a separate question.

The problem is the following: we have a set of axioms with negation as failure
semantics. We have a set of primary state variables P = {p_1, ..., p_m} and a
set of derived state variables D = {d_1, ..., d_n}. Let's assume that all state
variables are binary and that all derived variables are false unless derived
otherwise. (In Fast Downward it's a bit more complicated, but conceptually it's
easy to bring things into this form.)

So all derivation rules look like this:

    l_1, ..., l_k -> d_h

where each l_i is one of "p_j", "\neg p_j", "d_j" or "\neg d_j" for some index j.

We have the usual stratification constraints: we can assign a level to every
derived state variable such that

    level(d_i) <= level(d_j)
    whenever d_i occurs in the body of a rule with head d_j, and

    level(d_i) < level(d_j)
    whenever \neg d_i occurs in the body of a rule with head d_j.

We would ideally like to come up with an equivalent set of rules that are
expressed in terms of the negations of the d_i. That is, we want to introduce a
new set of variables \hat{d_i} and express new derivation rules in terms of
these variables instead of the hatless d_i variables such that when we evaluate
the rules, \hat{d_i} is true iff d_i is false.

Note that there is some freedom in how to assign the levels. We currently group
as many variables as possible into the same level. An alternative, which would
be more useful here and no harder to compute, would be to only group variables
in the same level if we absolutely have to, i.e., if we have a cyclic set of
constraints

   level(d_{i_1}) <= level(d_{i_2}) <= ... <= level(d_{i_n}) <= level(d_{i_1})

that forces all these levels to be the same. So let's assume we do that.

If all variables had different levels, the hat rules would be easy to define.

The rules for d_i would look like this:

   l_{1,1}, ..., l_{1,k_1} -> d_i
   ...
   l_{s,1}, ..., l_{s,k_s} -> d_i

where all literals l_{i,j} refer to primary state variables \neg d_j where
level(d_j) < level(d_i). (We can rule out the case where d_i itself occurs in
the body, which is strictly speaking allowed, by pruning such rules because they
can never fire unless d_i was already derived, in which case they don't
contribute anything.)

With an inductive argument, we can assume that we already know how to construct
rules for the \hat{d_j} of lower level, and in general we have that d_i is true
iff the DNF formula

    (l_{1,1} and ... and l_{1,k_1})
    or ... or
    (l_{s,1} and ... and l_{s,k_s})

is true, which means that d_i is false iff the formula

    (\neg l_{1,1} or ... or \neg l_{1,k_1})
    and ... and
    (\neg l_{s,1} or ... or \neg l_{s,k_s})

is true, which we can easily express as a CNF formula over the variables p_j and
\hat{d_j}.

So the problematic cases are only the ones where we have a cyclic dependency. In
a larger set of rules where some variables are at the same level and some are
not, we can deal with each of the cycles separately if we can come up with an
exact representation for the hatted variables.

If we can only come up with approximations of the \hat{d_i} variables (over or
under) locally for one cycle and we want to combine them into an approximation
(over or under) globally, I think we need to maintain *both* an over- and an
underapproximation because variables from earlier levels can be used in a
negated or non-negated way, and negation turns over- into underapproximations
and vice versa.

I think it should be possible to come up with an exact solution with a
polynomial blowup, which is probably too large for many of our benchmarks, but I
think might still be interesting from a theoretical perspective. More precisely,
the blowup would be by a factor of M, where M is the maximal number of derived
variables in the same layer (dependency cycle). The idea is to unroll the
variables over time to get rid of dependency cycles and observe that with M
variables in one cycle, we never need more than M time steps until we cannot
make any further derivations.

Consider Patrik's example from this issue. For consistency with the above,
rename the primary variable "P(bottom)" as p_1 and the derived variables Q(left)
as d_1, Q(right) as d_2 and Q(top) as d_3, our derivation rules are:

    \neg p_1 -> d_1
    \neg p_2 -> d_2
    d_1 -> d_3
    d_2 -> d_3
    d_3 -> d_1
    d_3 -> d_2

The last four rules force all d_i into the same level.

There are three variables, so let's create three copies d_{i,0}, ..., d_{i,2}
for each of them. We then replace the original rules by one or more copies as
follows:

If the LHS contains no variables from the cycle, create only one copy, where the
RHS variable gets time step 0.

Otherwise, create M-1 copies where the LHS has time steps {0, ..., M-2}, and the
RHS has the next time step. We also create "no-op" rules that allows us to
propagate the truth of a variable to the next time step. This gives us the
following new rules:

from the rules not involving cycle variables on the LHS:
    \neg p_1 -> d_{1,0}
    \neg p_2 -> d_{2,0}

from the rules involving cycle variables on the LHS:
    d_{1,0} -> d_{3,1}
    d_{1,1} -> d_{3,2}
    d_{2,0} -> d_{3,1}
    d_{2,1} -> d_{3,2}
    d_{3,0} -> d_{1,1}
    d_{3,1} -> d_{1,2}
    d_{3,0} -> d_{2,1}
    d_{3,1} -> d_{2,2}

no-op rules:
    d_{1,0} -> d_{1,1}
    d_{1,1} -> d_{1,2}
    d_{2,0} -> d_{2,1}
    d_{2,1} -> d_{2,2}
    d_{3,0} -> d_{3,1}
    d_{3,1} -> d_{3,2}

This new ruleset has no cycles any more, and we should be able to prove that we
can derive d_{i,M-1} iff we can derive d_i in the original set of rules.
Therefore we can use d_{i,M-1} in place of d_i in all later layers (where it is
treated like a primary variable).

Because the new rule set has no cycles, we can use it to compute the hatted
variables.

As I said, the blow-up is probably unacceptable in many cases, so let's also
briefly look at approximate solutions. I'll only talk about how to over- and
underapproximate on one cycle and from that we should be able to
over-/underapproximate for the whole set of rules. We will need separate
variables for the over/underapproximation, but let's ignore this here because I
only want to talk about one layer.

Let's return to our original set of rules:

    \neg p_1 -> d_1
    \neg p_2 -> d_2
    d_1 -> d_3
    d_2 -> d_3
    d_3 -> d_1
    d_3 -> d_2

If we want to overapproximate on this layer, a simple way is to replace all
occurrences of cycle variables on the LHS as "True"; to underapproximate, we
could use "False". For the overapproximation, this would give us:

    \neg p_1 -> d_1
    \neg p_2 -> d_2
    True -> d_3
    True -> d_3
    True -> d_1
    True -> d_2

This is quite drastic: it means that d_1, d_2, d_3 are always true, so it
trivializes and loses all information. The underapproximation is less drastic.
Having False on the LHS means dropping the rule entirely, so we get:

    \neg p_1 -> d_1
    \neg p_2 -> d_2
    

Which means that d_3 would always be False (an underapproximation), but at least
d_1 and d_2 would get their correct truth values. (The correct semantics for
this particular set of rules is that d_1, d_2, d_3 are all equivalent to (\neg
p_1 or \neg p_2.)

These approximations have the effect of breaking all the cycles, so we can again
compute (approximated) hatted versions based on these new rules.

But there is no need to be so drastic. We don't need to replace *all*
occurrences of cycle variables on the LHS by True (False) to over- (under-)
approximate. It is enough to replace sufficiently many of them to break all the
cycles.

For example, for the underapproximation, let's say we only replace the LHS
occurrences of d_3 with False, but not the ones of d_1 and d_2. Then we get:

    \neg p_1 -> d_1
    \neg p_2 -> d_2
    d_1 -> d_3
    d_2 -> d_3

This is acyclic, so we can compute the negation based on this, and it is
actually perfect. However, for the overapproximation, unless I overlooked
something, we cannot gain anything in this example by using True on the LHS
selectively: any way of breaking the cycles will make the rules trivial.

Of course the over/underapproximation and unrolling ideas can also be combined.
If we have a very large cycle, we could try to approximate it a bit to break it
into a smaller cycle, which we can then unroll.


That's all I have. I hope I didn't make a major mistake that makes the whole
concept invalid. If this works, it's probably well known in logic
programming/answer set programming/etc. circles, and it would be good to talk to
an expert in this area to find out if they know more about this problem, e.g. if
they have better approximations or more compact ways to compute the exact result.
msg8040 (view) Author: malte Date: 2018-11-04.04:09:51
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 "issue453", 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.
msg3332 (view) Author: patrik Date: 2014-08-21.03:10:16
I updated the alternative translator to the current sas-file format, and it
seems to work. Attaching the translated file (.sas) and the result of running
the preprocessor on this file (.pre). Running A*/blind with the resulting
preprocessed file produces the expected plan.
msg3323 (view) Author: malte Date: 2014-08-18.11:06:54
> Just to clarify: This is only a translator issue? In other words, provided a
> "direct" translation of axioms (i.e., just grounding and simplifying them to
> the required form), the basic search framework (successor generator, etc)
> should work?

Possibly; I'm not entirely sure. It could be the case that some of the later
code relies on the presence of the negated axioms for relevance analysis, i.e.,
the preprocessor might wrongly determine that a variable is irrelevant if the
negated axiom rules are absent. I hope I'll be able to look into this on Wednesday.
msg3322 (view) Author: patrik Date: 2014-08-18.04:58:24
Just to clarify: This is only a translator issue? In other words, provided a
"direct" translation of axioms (i.e., just grounding and simplifying them to the
required form), the basic search framework (successor generator, etc) should work?

From our perspective, the best (short-term) fix may be to dust off one of my
alternative translators and bring it up to date with the current FDR format.
msg3321 (view) Author: malte Date: 2014-08-17.11:36:20
I opened a separate issue for getting rid of the negated axiom rules (issue454),
as I'm not sure this is the only thing going on here, but that bit will be quite
a bit of work by itself. (Didn't add you to the nosy list, so please do if you
want to follow this.)
msg3319 (view) Author: malte Date: 2014-08-17.09:12:59
Agreed. It's also a question of the relative amount of work and time available
in the immediate future, though -- it may be quite a bit less work to fix the
current implementation without changing the architecture.
msg3318 (view) Author: patrik Date: 2014-08-17.03:15:11
Thanks for the detailed explanation!

So, a quick workaround would be to trick the translator into believing that the
positive of the derived Q predicate is relevant. I tried this, by adding a dummy
operator identical to the existing set-p except it has an extra parameter ?y and
the precondition (secondary-q ?y). This problem is indeed solvable :)

I don't think it's for me to tell you how to solve the problem, but it seems
that keeping the translation mechanism simple and correct (and, if necessary,
computing the reformulated axiom set on demand, storing it separately, and using
where it is helpful) would be a more modular solution. Working out the
semantically correct way of reasoning about negative axioms - particularly in a
relaxed setting - is indeed interesting (in fact, that's the reason we're now
looking at these problems...) but also possibly quite tricky. I'm not sure if it
can be done in standard logic, or if it requires something else (like
well-founded semantics/answer-set programming, etc).
msg3317 (view) Author: malte Date: 2014-08-16.10:27:43
Thanks, Patrik! I think this is a conceptual error in the translator.
I'll try to explain what I think is going on. I'm adding Gabi because
we recently discussed this part of the translator.


The grounded problem has the following structure:

one non-derived fact P(bottom), initially false.

three derived facts Q(left), Q(right), Q(top) with derivation rules:

not P(bottom) => Q(left)
not P(bottom) => Q(right)
Q(left) => Q(top)
Q(right) => Q(top)
Q(top) => Q(left)
Q(top) => Q(right)

one action:

PRE: nothing; EFF: P(bottom)

goal:

not Q(top)


Solving the problem requires relying on negation by failure, i.e.,
finding a state in which "not Q(top)" is *not* derived. The way that
the above derivation rules are phrased is "indirect" in the sense that
they don't directly tell us how to derive the literal "not Q(top)".
They only tell us how to derive the complementary literal "Q(top)".

For mostly historical reasons (this is not used by most heuristics),
the translator attempts to rephrase this in a more "active" way, by
giving derivation rules for "not Q(top)" instead of "Q(top)". This is
described briefly in the Fast Downward paper (but not the translator
paper) in Section 5.1.

The basic idea of this rephrasing is as follows: we can try to think
of derivation rules as defining a condition in DNF. For example, let's
say we have:

A and B => X
A and C => X
B and D => X

We can view this as X being defined by

(A and B) or (A and C) or (A and D).

The condition for "not X", then, is the negation of this formula:

    not ((A and B) or (A and C) or (A and D))

which we can then convert to DNF again if we want.


The problem with this is that this simple "negate the CNF" view of
derivation rules is problematic -- or at least we have to be much more
careful about it -- if there are cycles in the derivation rules. In
the task that is causing the problem, we can write the "CNF
definitions" as:

    Q(left)   if   not P(bottom) or Q(top)
    Q(right)  if   not P(bottom) or Q(top)
    Q(top)    if   Q(left) or Q(right)

From this the translator generates the negated rules:

    not Q(left)   if   P(bottom) and not Q(top)
    not Q(right)  if   P(bottom) and not Q(top)
    not Q(top)    if   not Q(left) and not Q(right)

and detects that it only ever needs the negated versions of Q(...) to
satisfy preconditions, goals or conditions in derivation rules. It
then decides that it should use *these* rules as the actual derivation
rules and use the *positive* literals as the negation-by-failure
fallback values. That is, to evaluate derived variables in a state, it
first assumes that all P(...) are *true* and uses the rules above to
try to derive *false* literals. Due to the cyclic dependency (deriving
"not Q(top)" requires "not Q(left)", which in turn requires "not
Q(top)"), this won't work.


I see two main possibilities for how to proceed here:

1. Think about what the proper semantics for these negated axioms
   should be in case of cycles and implement this.

2. Rip the negated axiom things out completely, as it is hardly used.
   (I think the causal graph heuristic benefits from it, but this
   might be about it.)
msg3316 (view) Author: patrik Date: 2014-08-16.03:28:28
FD reports attached problem unsolvable, but it has a valid plan. It seems that
the cause of this is an incorrect computation of the derived predicates. In the
second state (after applying the single action in plan), all the derived
predicates are true, which they should not be. (Also attaching fd-val, which I
used to check this; unfortunately, it doesn't print anything about axiom
evaluation.)

I have not checked if the axioms in the translated SAS file are correct.
History
Date User Action Args
2019-06-14 14:29:41maltesetsummary: 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.) Check for references to "issue453" in the code, specifically axiom_rules.py. TODOs: 1. Have a translator option that implements the new strategy with the trivial overapproximation. Make sure that relaxed reachability and relevance analysis play nicely with this. Make sure that the axiom evaluator in the search code ignores the fake rules. (In general, to make this work also with the old behaviour, we can ignore all rules where the head is the default value of the variable.) 2. Later, we probably want to try more sophisticated things, e.g. don't overapproximate if there are no cycles. -> See meta-issue: issue924. 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.) Check for references to "issue453" in the code, specifically axiom_rules.py. TODOs: 1. Have a translator option that implements the new strategy with the trivial overapproximation. Make sure that relaxed reachability and relevance analysis play nicely with this. Make sure that the axiom evaluator in the search code ignores the fake rules. (In general, to make this work also with the old behaviour, we can ignore all rules where the head is the default value of the variable.) 2. Later, we probably want to try more sophisticated things, e.g. don't overapproximate if there are no cycles.
2019-06-12 23:16:19maltesetmessages: + msg8893
2019-06-12 14:47:00augustosetmessages: + msg8882
2019-06-07 12:00:57salomesetmessages: + msg8865
2019-06-06 16:05:17augustosetmessages: + msg8851
2019-06-06 15:38:20maltesetmessages: + msg8849
2019-06-06 15:21:32salomesetmessages: + msg8848
2019-06-06 15:19:09maltesetmessages: + msg8847
2019-06-06 15:14:10augustosetmessages: + msg8846
2019-06-06 15:00:49maltesetmessages: + msg8845
2019-06-06 14:54:30augustosetmessages: + msg8844
2019-06-05 19:33:03maltesetmessages: + msg8819
2019-06-05 15:07:29augustosetmessages: + msg8810
2019-06-04 11:11:10maltesetnosy: + jendrik
messages: + msg8795
summary: 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.) Check for references to "issue453" in the code, specifically axiom_rules.py. -> 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.) Check for references to "issue453" in the code, specifically axiom_rules.py. TODOs: 1. Have a translator option that implements the new strategy with the trivial overapproximation. Make sure that relaxed reachability and relevance analysis play nicely with this. Make sure that the axiom evaluator in the search code ignores the fake rules. (In general, to make this work also with the old behaviour, we can ignore all rules where the head is the default value of the variable.) 2. Later, we probably want to try more sophisticated things, e.g. don't overapproximate if there are no cycles.
2019-06-03 17:06:25augustosetnosy: + salome, augusto
messages: + msg8790
2018-12-08 13:24:43maltesetmessages: + msg8206
summary: Check for references to "issue453" in the code, specifically axiom_rules.py. -> 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.) Check for references to "issue453" in the code, specifically axiom_rules.py.
2018-11-04 07:05:43maltesetmessages: + msg8047
2018-11-04 04:09:51maltesetmessages: + msg8040
summary: Check for references to "issue453" in the code, specifically axiom_rules.py.
2014-10-04 19:32:46maltesetkeyword: + translator
2014-08-21 03:10:27patriksetfiles: + disjunction2.pre
2014-08-21 03:10:16patriksetfiles: + disjunction2.sas
messages: + msg3332
2014-08-18 11:06:54maltesetmessages: + msg3323
2014-08-18 04:58:24patriksetmessages: + msg3322
2014-08-17 11:36:20maltesetmessages: + msg3321
2014-08-17 09:12:59maltesetmessages: + msg3319
2014-08-17 03:15:11patriksetmessages: + msg3318
2014-08-16 10:27:43maltesetstatus: unread -> chatting
nosy: + gabi
messages: + msg3317
2014-08-16 03:29:55patriksetfiles: + fd-val.cc
2014-08-16 03:29:03patriksetfiles: + disjunction2.soln
2014-08-16 03:28:49patriksetfiles: + disjunction2.pddl
2014-08-16 03:28:28patrikcreate