IJCAI 19

Full paper

Section: Framework, generic defs & motivation (Joerg + Dan)

Discussion on Plan-Property Dependencies 1 and 2.

What is a plan property?

• Plan property: polytime-computable Boolean fn of task Pi and applicable action sequence vec_a

What is a plan-property dependency?

• Basic dependency: p entails q if, for every applicable action sequence vec_a, if p(veca)=true then q(veca)=true, We say in this case that the basic dependency "p entails q" is valid in Pi.
• (Complex/general) dependency: propositional formula phi over plan properties. phi holds if, for every applicable action sequence vec_a, phi evaluates to true on vec_a. We say in this case that phi is valid in Pi. Basic dependencies are the special case "p ==> q". Motivation: this could be inside a single new plan prop. However, plan props are black boxes to the framework; in the exploration of composed dependencies, i.e. when solving the explanation problem specified below, the explanation facility will establish the interesting combinations across these blackboxes.

Entailment over two dependencies phi and psi: phi entails psi if, for every action sequence, if phi evaluates to true then so does psi. Note that this is equivalent to validity of the dependency "phi ==> psi".

show that dependencies, and entailment thereover, are more than standard propositional logic: even if a formula is not universally true, iot may be true for all action sequences due to the underlying planning task. In fact this will typically be the case, e.g. in a simple mutex where reaching one fact A excludes reaching another fact B.

What is the explanation problem that we tackle here?

• basic: find all pairwise dependencies, ie, compute the graph whose nodes are the properties and whose edges are the basic dependencies
• general: find all strongest dependencies: the root nodes in the DAG over equivalence classes of dependencies

Motivation

Needs to be done carefully!

Place our approach and the kinds of explanations it provides relative to the literature (contrastive explanations). Which are the kinds of user questions that we can answer?

All this relates closely to propositional logic, to mutex analysis, to invariants more generally.

Relation to model checking ie asking questions about properties of planning task? Joerg thinks it's basically a special case, formulating a relevant analysis and implementing that effectively.

Use trucks/packs with fuel as canonical simple running example; but also more complex ones/beyond, inspired by proposal

Section Simple Instantiation goal-set conflicts

as per draft (Rebecca + Michael)

Section Compilation into goal-set conflicts

more general plan props and how they can be compiled into previous.

compilability:

given task Pi = (V,A,I) and plan property phi. design in polynomial time a task Pi' = (V',A',I') where V subseteq V' and A subseteq A' so that:

1. for every applicable action sequence veca' in Pi' leading to state s', the A-subsequence veca of veca' is applicable in Pi and leads to a state s that agrees with s' on V;
2. there is a state var v' in V' \setminus V such that, for every applicable action sequence veca' in Pi' leading to state s', v' is true in s' if and only if veca as per 1. satisfies phi in Pi.

research question: which known compilations can be done in this way?

• LTL over state variables: presumably only safety properties ie representable by finite automaton; is there a syntactic characterization of that fragment? Compilation into PDDL-style planning prior work Edelkamp (for MIPS IPC 2006), McIlraith (a few papers after 2005/6); presumably the comöilations there can be used as-is, with adaptations to fit the single-state-var v' setup we need here. Inductive definition of compilations? Given previous compilations Pi_phi and Pi_psi for subformulas phi and psi, define the compilation for a combination of phi and psi? Properties 1. and 2. above should be preserved transitively, need to check.
• action subsets used in plan? eg is an instance of some action schema used? are actions from two different subset classes (eg using truck1 and using truck2) used? general formulation: propositional logic whose atoms are "plan uses at least one action from A'" where A' subseteq A. Compilation: one flag for each A', set by actions from A' in plan; formula checking step at end.

Section experiments

on both simple instantiation (oplan properties are goal facts), and on compiled more general plan props.

comparison to baselines/other solvers:

can be done relative to solving simpler problems, specifically a) oversubscription planning ie finding a maximum-size solvable goal subset, and/or b) classical planning for a solvable goal set.

benchmarks:

simple, ie plan properties are goal facts:

RCP (resource-constrained planning) domains from Marcel's previous work: NoMystery, TPP, Rovers.

Ideally, we should actually do something with existing oversubscription planning benchmarks. Carmel and Mirkis generated ones in their work (http://iew3.technion.ac.il/~dcarmel/Papers/Sources/ecai14b.pdf), from IPC benchmarks, by restricting plan cost to 25%, 50%, 75%, and 100% of optimal plan cost for all goals. Emulate this, for unit action costs, in a way that makes our current technology applicable. Question: what about the nogood learning here? does the search just prune against the g function? or do we represent a discrete g function through a discrete state variable treating it like a resource?

LTL plan properties:

IPC 2006 planning with temporal goals; make these oversubscribed problems and do the same as above. does this work with those benchmarks?

Temporal ordering over actions: plan uses A before B etc, easily expressed by/compiled into LTL over state variables. eg Logistics: why are you delivering packageA before packageB?

action subsets used in plan:

NoMystery: extension of the above where the new plan property is using only one specific truck (truck1, truck2), or using only a single truck (no matter which one). Another possibility: package1 and package2 should be delivered using the same truck (load/unload package1 on truckX excludes löoad/unload package2 on truckY).

Similar in TPP, Rovers; so far as there is >1 vehicle. Maybe variants with just one central fuel/energy store so we don't get into the pareto-optimality issue? Also an idea is to restrict to particular scalable instance family where the optimal amount of fuel/energy is known by construction; could be much easier to write generators for this.

Plan property of the form "plan uses an action from B and does not use an action from A" (because user is asking "why does the plan include an action from A rather than one from B?"): eg Logistics why is packageX transported with truckA not with truckB? why image with RoverA not RoverB?