Fully-Automated Instance Decomposition and Subplan Synthesis for Parallel Execution

Subplans with limited interactions can be executed in a parallel and flexible manner. Given the success of SAT planning in the international planning competitions in 2004 and 2006 and advances in SAT solving, it is worth investigating how SAT planning can be used to generate plans for execution by multiple agents. We report on SAT encodings that have a model if and only if there are n subplans, each with up to k steps, such that they together achieve the goal and also satisfy the encoded criteria about permitted and prohibited interactions among them. These n subplans can be executed by different agents. Our SAT-based approach decomposes a planning instance fully automatically in an entirely unfamiliar domain with no knowledge from humans, if a decomposition exists. Desired properties of decomposition and solution are encoded as SAT. The key ideas in our encodings are an allocation of actions and subgoals to various agents and explanatory frame axioms for multiple agents. No domain-specific knowledge is used. We report on an empirical evaluation of the encodings. Our approach is domain-independent and fully automated. We discuss variants of our encodings.