Created on 20140816.03:28:28 by patrik, last changed by salome.
See metaissue: 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.

msg9197 (view) 
Author: salome 
Date: 20200213.12:33:51 

I ran experiments for all possible configurations of the options detailed in the meta issue. To reiterate we had the following options:
1. layer strategy (how many axiom layers should we create):
a) max
b) min (current implementation)
2. overapproximate negated axioms:
a) all: trivial overapproximation for all literals
b) cycles: trivial overapproximation for literals with cyclic dependencies
c) none: negate all axiom rules exactly (current implementation, leads to bugs)
3. overapproximate necessary literals:
a) exact: do a full relevance analysis
b) nonderived: consider all nonderived literals (both positive and negative) as necessary
c) positive: only consider positive nonderived literals as necessary (current implementation)
4. keep redundant axioms (if a derived variable is only needed negatively, should we keep the positive axiom rules or not?)
a) no (current implementation)
b) yes
I tested both blind and ff search, and also tested the problems uploaded to the various issues mentioned in the meta issue (issue924). The results can be found here:
https://ai.dmi.unibas.ch/_tmp_files/simon/issue453v2.html
https://ai.dmi.unibas.ch/_tmp_files/simon/issue453v2custompddls.html
Since the tables are nearly impossible to parse due to the amount of configurations, I also made some plots which try to highlight the influnece of different options:
https://ai.dmi.unibas.ch/_tmp_files/simon/issue453v2figures.pdf
Overall I see the following trends:
 Using the minimum amount of axiom layers seems to be faster in general (especially visible for blind search). The only reason I found that could possibly explain this is msg3058. Essentially, the code does not apply negation by failure rules in the last iteration, and I guess if the layer is smaller then we do not save as much time with this optimization. But I am very unsure about details here.
 Overapproximating negated axiom rules for literals in cycles resolves the bug from this issue. It does negatively influence the ff heuristic in some rare cases, but I would say this is a small price to pay for removing a bug .
 Overapproximating all negated axiom rules does very noticeably influence the ff heuristic (no suprises there).
 The type of relevance analysis does not seem to influence the time the translator needs nor overall coverage all that much.
 Keeping redundant positive axioms does not hurt task size significantly, in the worst cases it results in about a 50% bigger task file.

msg8893 (view) 
Author: malte 
Date: 20190612.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
tradeoff not to compute any notion of "necessary" at all.

msg8882 (view) 
Author: augusto 
Date: 20190612.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: 20190607.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: 20190606.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 outofmemory 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 outofmemory for
our normal version but is solved in less than one second by the
overapproximation version. The same happens for Patrik's
"crashdummydomain.pddl" variant of this domain.
 the graph domain runs outofmemory 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: 20190606.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: 20190606.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: 20190606.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: 20190606.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: 20190606.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: 20190606.14:54:30 

The results are in
http://inf.ufrgs.br/~abcorrea/_issues/issue453/issue453v1.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 airportadl. I am running a new experiment only
with airportadl. 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 hvalues). It is interesting to see that
the causal graph heuristic (cg) is significantly more informed than the
deletefree heuristics in a few domains when using the overapproximation approach.
We also have an instance of psrlarge where the translator runs outofmemory in
our overapproximation, which is very bad since the "normal" version multiplies
out the CNF and still doesn't run outofmemory. 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: 20190605.19:33:03 

As discussed offline: msg8235 lists the axiomrelated 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: 20190605.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 deleterelaxation 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: contextenhanced additive heuristic, causal graph heuristic, FF
heuristic, LMcount 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: 20190604.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 lefthand 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: 20190603.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 deletefree 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 "nondeterminism" 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: 20181208.13:24:43 

Add a pointer to msg8204 to the summary.

msg8047 (view) 
Author: malte 
Date: 20181104.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 nonnegated 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 M1 copies where the LHS has time steps {0, ..., M2}, and the
RHS has the next time step. We also create "noop" 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}
noop 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,M1} iff we can derive d_i in the original set of rules.
Therefore we can use d_{i,M1} 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 blowup 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: 20181104.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: 20140821.03:10:16 

I updated the alternative translator to the current sasfile 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: 20140818.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: 20140818.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 (shortterm) 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: 20140817.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: 20140817.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: 20140817.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 setp except it has an extra parameter ?y and
the precondition (secondaryq ?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
wellfounded semantics/answerset programming, etc).

msg3317 (view) 
Author: malte 
Date: 20140816.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 nonderived 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 negationbyfailure
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: 20140816.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 fdval, 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.


Date 
User 
Action 
Args 
20200213 12:33:51  salome  set  messages:
+ msg9197 
20190614 14:29:41  malte  set  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.
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 metaissue: 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. 
20190612 23:16:19  malte  set  messages:
+ msg8893 
20190612 14:47:00  augusto  set  messages:
+ msg8882 
20190607 12:00:57  salome  set  messages:
+ msg8865 
20190606 16:05:17  augusto  set  messages:
+ msg8851 
20190606 15:38:20  malte  set  messages:
+ msg8849 
20190606 15:21:32  salome  set  messages:
+ msg8848 
20190606 15:19:09  malte  set  messages:
+ msg8847 
20190606 15:14:10  augusto  set  messages:
+ msg8846 
20190606 15:00:49  malte  set  messages:
+ msg8845 
20190606 14:54:30  augusto  set  messages:
+ msg8844 
20190605 19:33:03  malte  set  messages:
+ msg8819 
20190605 15:07:29  augusto  set  messages:
+ msg8810 
20190604 11:11:10  malte  set  nosy:
+ 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. 
20190603 17:06:25  augusto  set  nosy:
+ salome, augusto messages:
+ msg8790 
20181208 13:24:43  malte  set  messages:
+ 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. 
20181104 07:05:43  malte  set  messages:
+ msg8047 
20181104 04:09:51  malte  set  messages:
+ msg8040 summary: Check for references to "issue453" in the code, specifically axiom_rules.py. 
20141004 19:32:46  malte  set  keyword:
+ translator 
20140821 03:10:27  patrik  set  files:
+ disjunction2.pre 
20140821 03:10:16  patrik  set  files:
+ disjunction2.sas messages:
+ msg3332 
20140818 11:06:54  malte  set  messages:
+ msg3323 
20140818 04:58:24  patrik  set  messages:
+ msg3322 
20140817 11:36:20  malte  set  messages:
+ msg3321 
20140817 09:12:59  malte  set  messages:
+ msg3319 
20140817 03:15:11  patrik  set  messages:
+ msg3318 
20140816 10:27:43  malte  set  status: unread > chatting nosy:
+ gabi messages:
+ msg3317 
20140816 03:29:55  patrik  set  files:
+ fdval.cc 
20140816 03:29:03  patrik  set  files:
+ disjunction2.soln 
20140816 03:28:49  patrik  set  files:
+ disjunction2.pddl 
20140816 03:28:28  patrik  create  
