Abstract:
Optimal planners in the classical setting are built around two notions: branching and pruning. SAT-based planners for example branch by trying the values of a selected variable, and prune by propagating constraints and checking consistency. In the conformant setting, a similar branching scheme can be used if restricted to action variables, but the pruning scheme must be modified. Indeed, pruning branches that encode inconsistent partial plans is not sufficient since a partial plan may be consistent and complete (covering all the action variables) and still fail to be a conformant plan. This happens indeed when the plan does not conform to some possible initial state or transition. A remedy to this problem is to use a criterion stronger than consistency for pruning. This is actually what we do in this paper where the consistency-based pruning criterion used in classical planning is replaced by a validity-based criterion suitable for conformant planning. Under the assumption that actions are deterministic, a partial plan can be defined as valid when it is logically consistent with the theory and each possible initial state. A valid partial plan that is complete is guaranteed to encode a conformant plan, and vice versa. Checking validity, however, while useful for pruning can be very expensive. We show then that such validity checks can be performed in linear time provided that the theory encoding the problem is transformed into a logically equivalent theory in deterministic decomposable negation normal form (d-DNNF). In d-DNNF, plan validity checks can be reduced to two linear-time operations: projection (finding the strongest consequence of a formula over some of its variables) and model counting (finding the number of satisfying assignments). We then define and evaluate a conformant planner that branches on action variables, and prunes invalid partial plans in linear time. The empirical results are encouraging, showing the potential benefits of stronger forms of inference in planning tasks that are not reducible to SAT.