SAT-Based Reasoning for Classical Planning with Parallel Actions
Handbook of Satisfiability - Chapter 19

Planning in artificial intelligence is the process of a valid sequence of actions that reaches a predifined goal. The problem is usually expressed in terms of a description of a initial state, a set of actions and a final goal state. The most basic form of planning is called "cassical planning", where there is only one initial state and all of the actions are deterministic.

Kautz and Selman suggested, in 1992, that classical planning problem could be solved by translating it into a propositional logic formula and testing if its satisfiability.

The classical planning problem is PSPACE-complete, os there are presumably no polynomial time translations from classical planning to SAT. The formulae that that represents the classical planning problem may, in the wrost case, be exponential in the size of the problem instance.

The fundamental idea of using SAT for planning is to encode a plan of a given lengh \(n\) as a formula in the classical propositional logic. The formula for a given \(n\) is satisfiable if and only if there is a plan of size \(n\).

Planning is consider a setting where the states of the world are represented in terms of a set \(X\) of boolean state variables which take the values \(true\) or \(flase\). Formulae are formed from the state variables with connectives \(\lor\) and \(\lnot\). The connectives \(\land\), \(\rightarrow\) and \(\leftrightarrow\) are defined in terms of \(\lor\) and \(\lnot\).

A \(literal\) is a formula of the form \(x\) or \(\lnot x\) where \(x \in X\). A \(clause\) is a disjunction of one or more literals. There is also the constants atoms \(\top\) and \(\perp\) for denoting \(true\) and \(false\), respectively.

Each \(state s:X\rightarrow {0,1}\) assigns each state variable in \(X\) a value 0 or 1, while the actions will change the state of the world.

Action Definition An \(action\) over a set of state variables \(X\) is a pair \(\langle p,e \rangle\) where

1. \(p\) is a propositions formula over \(X\) (the precondition) and
2. \(e\) is a set of pairs \(f \implies d\) (the effects) where \(f\) is a propositional formula over \(X\) and \(d\) is a set of literals over \(X\).

An important factor in the efficiency of SAT-based planners is the notion of parallel plans. Hardly a plan is purely sequential in the sense that any two consecutive actions have to be in the given order. For example, the last two actions in a plan for achieving \(a \land b\) could respectively make \(a\) and \(b\) true and be completely independent of each other. Therefore, the ordering of the actions can be change without invalidating the plan.

The most commonly used measure for plan quality is the number of actions in the plan. So the problem of finding an optimal plan is the problem of finding the shortest sequential plan, in terms of the satisfiability, finding an integer \(t\) such that the formula for plan length \(t − 1\) is unsatisfiable and the formula for plan length \(t\) is satisfiable.

For parallel plans the question is more complicated. It is possible to find an optimal parallel plan for a given parallel length by using cardinality constraints on the number of actions in the plans, but it seems that finding an optimal parallel plan in the worst case reduces to testing the existence of sequential plan: if there is a parallel plan with \(t\) time points and \(n\) actions, the optimality test may require testing whether there is a sequential plan with \(n − 1\) time points and \(n − 1\) actions. Tests restricting to formulae with \(t\) time points are not sufficient.