how to interpret the result of invariant_finder.py ?

[Aymeric]

Hello all,

I am trying to find constraints in the states and/or actions of a planning problem. I already have the two pddl files (domain and problem, click to see), and I want to use Fast Downward to output existing constraints/invariants.

Example of constraints I would like to find:

- An invariant of one of the predicates (i.e., a predicate that is always True or always False whatever the state)

- An invariant between a precondition and an effect (i.e : x1 True in precondition ---> x2 True in effect)


I have run this command:

    python  invariant_finder.py domain.pddl problem.pddl

And here is the output:


Parsing...
Normalizing...
Finding invariants...
NOTE: not passing in reachable_action_params.
This means fewer invariants might be found.
256 initial candidates
{z2 }
{z8 }
{z9 }
{z10 }
{z13 }
{z14 }
{z16 }
{z36 }
{z39 }
{z47 }
{z51 }
{z60 }
{z62 }
{z78 }
{z85 }
{z116 }
{z122 }
{z134 }
{z147 }
{z152 }
{z154 }
{z171 }
{z176 }
{z182 }
{z184 }
{z190 }
{z193 }
{z211 }
{z216 }
{z224 }
{z225 }
{z247 }
{z266 }
{z270 }
{z272 }
{z290 }
{z291 }
{z293 }
{z296 }
Finding fact groups...
Finding invariants...
256 initial candidates


Finding invariants: [29.250s CPU, 29.428s wall-clock]
Checking invariant weight... [0.000s CPU, 0.000s wall-clock]
[Atom z216()]



What does this output of predicates ( {z2} {z8} ...) corresponds to ? Does it mean that each of these variable is always True whatever the state ?

What does "Checking invariant weight..." stands for ? Why does it output Atom z216() ?

Thank you for your help

Aymeric

p.s: for those interested these pddl were generated by LatPlan

[Florian Pommerening]

Hi Aymeric,


we recently had a discussion about this output on the Fast Downward
Discord channel. I'm not too familiar with this part of the code, so let
me quote Malte from that discussion:

> {at-robby [0]}
> {at 0 [1], carry 0 [1]}
> {free 0, carry 1 [0]}
>
> The syntax is cryptic, unfortunately. The second one means, for
> example, that for every object x, the number of other objects it's at
> or that carry it, can never increase. This is the basis on which we
> create the finite-domain variables, so if you trace this information
> through the variable instantiation, it might be useful.

So in your case, the invariants like {z2 } show no parameters and there
is only one predicate in each line. I think what this means is that
"z2" does not have any parameters and once it is false, it cannot become
true anymore. Formally, the number of facts instantiating predicates
from the set {z2} cannot increase, and since there is only one fact that
can instantiate z2, this means that once it is false, the number is 0
and cannot increase again by making this fact true.

As far as I know, the "weight" of an invariant candidate is the number
of facts instantiating predicates from that candidate. If the weight can
increase by applying the action, the candidate is no a invariant, and
more predicates are added to it. If the weight of a candidate can only
decrease, and is 1 in the initial state, it is an invariant. Fast
Downward then creates finite-domain variables from such invariants. For
an invariant {d1, d2, d3}, it would create a variable with domain {d1,
d2, d3, <none-of-those>}. In cases where it can prove that the weight
can also not decrease (so it will remain constant), we do not need the
<none-of-those> value.

Cheers
Florian

On 02.10.22 17:39, 'Aymeric' via Fast Downward wrote:
> Hello all,
>
>
> I am trying to find constraints in the states and/or actions of a
> planning problem. I already have the two pddl files (domain

> <https://raw.githubusercontent.com/aymeric75/latplan/main/domain.pddl>and problem
> <https://raw.githubusercontent.com/aymeric75/latplan/main/problem.pddl>,

> click to see), and I want to use Fast Downward to output existing
> constraints/invariants.
>
>
> Example of constraints I would like to find:
>
> - An invariant of one of the predicates (i.e., a predicate that is
> always True or always False whatever the state)
>
> - An invariant between a precondition and an effect (i.e : x1 True in
> precondition ---> x2 True in effect)
>
>
> I have run this command:
>
>     python  invariant_finder.py domain.pddl problem.pddl
>
> And here is the output:
>

> /

> /

>
> What does this output of predicates ( {z2} {z8} ...) corresponds to ?
> Does it mean that each of these variable is always True whatever the state ?
>
>
> What does "Checking invariant weight..." stands for ? Why does it output
> Atom z216() ?
>
>
> Thank you for your help
>
> Aymeric
>
>
> p.s: for those interested these pddl were generated by LatPlan

> <https://github.com/guicho271828/latplan>
>
> --
> You received this message because you are subscribed to the Google
> Groups "Fast Downward" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to fast-downwar...@googlegroups.com
> <mailto:fast-downwar...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/fast-downward/232edc25-da59-4a0d-be8c-bc6f957bb6e0n%40googlegroups.com
> <https://groups.google.com/d/msgid/fast-downward/232edc25-da59-4a0d-be8c-bc6f957bb6e0n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Malte Helmert]

Hi Aymeric,

adding to what Florian mentioned: some of the things you mention in your
email are not what we call "invariants" in Fast Downward, so you might
also get answers from other parts of the planner. For example, if the
translator detects that certain atoms will always be true or always be
false, it fill substitute the truth value wherever the atom occurs and
remove it from the task completely.

So if you want to know more about these things, we can perhaps tell you
more if you give us more information on what exactly you are looking
for. In this case it could also help if you included example PDDL inputs
as an attachment or link, so that we can also run things ourselves and
illustrate our answer with an example.

Best,
Malte