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