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