Issue453

Title Solvable problem reported unsolvable - incorrect computation of derived predicates?
Priority bug Status chatting
Superseder Nosy List gabi, malte, patrik
Assigned To Keywords translator
Optional 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.

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

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