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.
