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

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

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