Fundamentals of Automated Planning

When it comes to solvers, a SAT solver is a computer programme which aims to resolve Boolean satisfiability problems (SAT formulas). Basically, it takes a Boolean formula as input, such as \((x_0 \lor x_1) \land (x_0 \lor \lnot x_1)\), and outputs whether the formula is satisfiable, meaning that there are possible values of \(x_0\) and \(x_1\) which make the formula true, or unsatisfiable, meaning that there are no such values of \(x_0\) and \(x_1\), which make the formula true.

The formula received is in CNF. The CNF is a standardised way of writing Boolean formulas in logic, where the formula is composed of a conjunction (AND, denoted as \(\land\)) of one or more clauses, and each clause is a disjunction (OR, denoted as \(\lor\)) of literals (a variable or its negation). For example, \((x_0 \lor x_1) \land (x_0 \lor \lnot x_1)\) is in CNF.

The decision-making challenge in propositional logic, often known as the (SAT) problem, is famously NP-complete (Cook, Stephen A, 2023). While NP-completeness suggests (assuming the reasonable hypothesis that \(P \neq NP\)) that any comprehensive SAT algorithm operates in exponential time in the worst-case scenario, SAT solvers frequently perform better than this worst-case prediction. Numerous algorithms have been developed over the years to tackle SAT problems. In this paper, we will examine some of these algorithms in the following sections.

Planners decompose the world into logical conditions and represent a state as conjunction of positive literals. We will consider propositional literals; for example, \(Poor \land Unknown\) might represent the state of a hapless agent. We will also use first-order literals; for example, \(At(Plane_1,Accra) \land At(Plane_2,Brasília)\), to represent a state in the package delivery problem.

Literals in first-order state descriptions must be ground and function-free. A literal is said to be ground if it contains no variables, that is, all its arguments are constants denoting concrete objects of the domain. This restriction ensures that states describe only fully instantiated facts rather than schematic or generic conditions. Moreover, literals must be function-free, meaning that no function symbols are allowed in their arguments; consequently, terms such as nested or composed expressions are excluded, and only constant symbols may occur. This guarantees a finite set of possible ground atoms and, therefore, a finite state space. An atom is a formula of the form \((P(t_1,\dots,t_n))\), where (\(P\)) is an (n)-ary predicate symbol and \((t_1,\dots,t_n)\) are terms; atoms constitute the most basic assertions about the domain and contain no logical connectives or quantifiers. A literal is either an atom or its negation. As a result, literals such as \(At(x,y)\) or \(At(Father(Fred),Brasília)\) are not allowed. The closed-world assumption is used, meaning that any conditions that are not mentioned in a state are assumed false.

A goal is a partially specified state, represented as a conjunction of positive ground literals, such as \(Rich \land Famous\) or \(At(P_2, Tahiti)\). A propositional state \(s\) \textbf{satisfies} a goal \(g\) if \(s\) contains all the atoms in \(g\) (and possibly others). For example, the state \(Rich \land Famous \land Miserable\) satisfies the goal \(Rich \land Famous\).

An action is specified in terms of the preconditions that must hold before it can be executed and the effect that ensue when it is executed. For example, an action for flying a plane from one location to another is:

To facilitate interoperability and benchmarking within the automated planning community, the PDDL (Drew McDermott and Michael Ghallab and Adele Howe and Craig Knoblock and Ashwin Ram and Manuela Veloso and Daniel Weld and David Wilkins, 1998) was developed as a unifying formalism. First introduced for the inaugural International Planning Systems Competition in 1998 (McDermott, Drew M, 2000), PDDL represented a collective endeavour led by leading researchers to provide a common framework for the specification of planning domains and problems. Since its inception, PDDL has undergone multiple revisions, with subsequent editions of the language introducing additional features aimed at accommodating a broader range of planning challenges, such as numeric reasoning and temporal constraints. These enhancements have often been motivated by the evolving requirements of the International Planning Competition (IPC, 1998) itself.

Although PDDL aspires to function as a shared modelling language, it should not be mistaken for an official standard. Its role is best seen as a community-driven approach to enabling the exchange and reuse of planning systems and models. The lack of a definitive and completely unambiguous specification, particularly given the variation in language versions and stylistic differences in supporting documentation, means that the interpretation of certain constructs can differ between planning systems. In practice, most planners implement only a subset of features from specific versions, sometimes interpreting ambiguous elements according to their own conventions.

Despite these variations, there exists a broadly recognised core within PDDL that is widely understood and utilised across the community. Discourse and scholarship generally centre on this consensus core, incorporating key aspects from various versions whilst eschewing features that are poorly supported or ambiguously defined. It is common practice to highlight areas where the semantics or syntax may be open to interpretation, ensuring that users of planning technology are aware of potential discrepancies between implementations.

The process of translating \(STRIPS\) problems into propositional logic exemplifies the knowledge representation cycle. This process commences with the establishment of a reasonable set of axioms, followed by the identification of any unintended models that may emerge, leading to the refinement of these axioms.

To illustrate this process, (Russell, Stuart J and Norvig, Peter, 2016) proposes a basic air transport problem. In the initial state (time \(0\)), plane \(P_1\) is situated at \(SFO\), while plane \(P_2\) is located at \(JFK\). The objective is to reposition \(P_1\) at \(JFK\) and \(P_2\) at \(SFO\), effectively facilitating a swap between the two aircraft. Distinct proposition symbols for each time step are required, with superscripts employed to denote the specific time. The initial state can be formally represented as

\(At(P_1, SFO)^0 \land At(P_2, JFK)^0\).

Given that propositional logic does not operate under a closed-world assumption, it is imperative to specify propositions that are not \(true\) in the initial state. In instances where certain propositions remain unknown, they may be left unspecified, thereby adopting an open-world assumption. In this particular example, the following propositions are specified:

\(\lnot At(P_1, JFK)^0 \land \lnot At(P_2, SFO)^0\).

The goal must be linked to a specific time step. As the number of steps required to achieve the goal is not known in advance, it is feasible to initially assert that the goal is true at time \(T = 0\), represented as \(At(P_1, JFK)^0 \land At(P_2, SFO)^0\). If this assertion fails, the process is repeated for \(T = 1\), and so forth, until the minimum feasible plan length is determined. For each value of \(T\), the knowledge base will encompass only the sentences relevant to the time steps from \(0\) to \(T\). To ensure the end of the algorithm, an arbitrary upper limit, \(T_\text{max}\), is established. This algorithm is illustrated in the following pseudo-code on Listing 1.

function SATPLAN(problem, T_max) returns solution or failure
    inputs: problem, a planning problem
    T_max, an upper limit for plan length
    for T = 0 to T_max do
        cnf, mapping <- TRANSLATE-TO-SAT(problem, T)
        assignment <- SAT-SOLVER(cnf)
        if assignment is not null then
            return EXTRACT-SOLUTION(assignment , mapping)
    return failure

The next challenge is to encode action descriptions within propositional logic. The most straightforward method is to assign a unique proposition symbol for each action occurrence; for example, \(Fly(P_1, SFO, JFK)^0\) is true if plane \(P_1\) flies from \(SFO\) to \(JFK\) at time \(0\). Propositional versions of the successor-state axioms are employed to represent these actions.

For instance, the relationship can be expressed as follows:

\(At(P_1, JFK)^1 \Leftrightarrow (At(P_1, JFK)^0 \land \lnot (Fly(P_1, JFK, SFO)^0 \land At(P_1, JFK)^0)) \lor (Fly(P_1, SFO, JFK)^0 \land At(P_1, SFO)^0)\).

This indicates that plane \(P_1\) will be at \(JFK\) at time \(1\) if it was at \(JFK\) at time \(0\) and did not fly away, or if it was at \(SFO\) at time \(0\) and flew to \(JFK\). It is necessary to formulate one such axiom for each plane, airport, and time step. Additionally, the inclusion of each new airport introduces further travel options to and from a given airport, thereby increasing the number of disjuncts on the right-hand side of each axiom.

With these axioms in place, we can run the satisfiability algorithm to find a plan. There ought to be a plan that achieves the goal at time \(T = 1\), namely, the plan in which the two planes swap places. Now, suppose the knowledge base (\(KB\)) is

\(\textit{initial state} \land \textit{successor-state axioms} \land \textit{goal}^1\),

which asserts that the goal is true at time \(T = 1\). You can check that the assignment in which

\(Fly(P_1, SFO, JFK )^0 \quad \text{and} \quad Fly(P_2, JFK, SFO)^0\)

are true and all other action symbols are false constitutes a model of the \(KB\). While this is a valid model, there may be other potential models that the satisfiability algorithm could yield. However, not all of these alternative models represent satisfactory plans. For instance, consider a rather trivial plan defined by the action symbols

\(Fly(P_1, SFO, JFK )^0 \quad \text{and} \quad Fly(P_1, JFK , SFO)^0 \quad \text{and} \quad Fly(P_2, JFK , SFO)^0\).

This plan is unreasonable because plane \(P_1\) departs from \(SFO\), making the action \(Fly(P_1, JFK, SFO)^0\) impossible. To prevent the creation of plans with invalid actions, we need to incorporate precondition axioms that require the preconditions to be met for an action to occur. For instance, we need to establish that:

\(Fly(P_1, JFK, SFO)^0 \Rightarrow At(P_1, JFK)^0\).

Since \(At(P_1, JFK)^0\) is indicated as false in the initial state, this axiom guarantees that \(Fly(P_1, JFK, SFO)^0\) is also set to false in every model. By adding these precondition axioms, there is only one model that fulfills all the axioms when the goal is to be achieved at time \(1\). This model involves plane \(P_1\) flying to \(JFK\) and plane \(P_2\) flying to \(SFO\). It is important to note that this solution consists of two parallel actions.

Introducing a third airport, LAX, leads to unexpected outcomes, as each plane now has two possible actions per state. Running the satisfiability algorithm reveals that existing axioms permit a plane to reach two destinations simultaneously, creating unrealistic solutions. To prevent this, additional axioms, such as action exclusion axioms preventing concurrent actions, must be added. For example, we can enforce complete exclusion by including all possible axioms of the form

\(\lnot(Fly(P_2, JFK, SFO)^0 \land Fly(P_2, JFK, LAX)^0)\).

These axioms guarantee that no two actions can be performed simultaneously, thereby removing all invalid plans. However, they also require every plan to be totally ordered, resulting in a loss of flexibility as partially ordered plans are no longer possible. Additionally, this may increase the number of time steps in the plan and thus lengthen computation time.

Exclusion axioms can sometimes appear rather blunt. Rather than stating that a plane cannot fly to two airports simultaneously, we might instead simply require that no object can be in two places at once:

\(\forall p, x, y, t \quad x \neq y \quad \Rightarrow \quad \lnot(At(p, x)^t \land At(p, y)^t)\) .

Planning is currently a highly active research area in AI, largely because it brings together the key concepts of search and logic discussed earlier. In essence, a planning system can be seen as either searching for a solution or as constructing a logical proof that a solution exists (Fikes, Richard E and Nilsson, Nils J, 1971). The interplay between these two fields has led to dramatic enhancements in efficiency over the past decade, resulting in planners being widely adopted in industry. However, it remains unclear which methods are most effective for particular types of problems, and it is likely that future approaches will surpass those we have today.

Planning is primarily about managing the challenges of combinatorial explosion. In a domain with \(p\) primitive propositions, there are \(2^p\) possible states. As the complexity of the domain grows, so can \(p\), making things even more daunting. When objects in the domain have various properties (such as Location or Colour) and take part in relations (like At, On, or Between), the number of possible states increases dramatically. For example, with \(d\) objects and ternary relations, there are \(2^{d^3}\) potential states. This makes it appear, at least in the worst case, that planning is an insurmountable task.

Despite such a gloomy outlook, the divide-and-conquer strategy can be highly effective. When a problem can be fully broken down into independent sub-problems, this method can result in exponential gains in efficiency. However, the presence of negative interactions between actions often disrupts this decomposability. Partial-order planners address these issues by explicitly representing causal links, but every conflict that arises must be resolved by deciding the sequence of actions, leading to a rapid increase in possible configurations.

In contrast, GRAPHPLAN² sidesteps explicit choices during graph construction by using mutex links to indicate conflicts, rather than immediately deciding how to address them. SATPLAN ² also manages these mutual exclusions but encodes them in general CNF form rather than through a dedicated structure. The effectiveness of this approach largely depends on the capability of the underlying SAT solver.

There are several strategies for managing combinatorial explosion. Techniques developed for controlling backtracking in constraint satisfaction problems (CSPs), such as dependency-directed backtracking, are equally applicable to planning. For instance, extracting a solution from a planning graph can be cast as a Boolean CSP, where each variable represents whether a particular action takes place at a specific time. These CSPs can be tackled with algorithms like min-conflicts (Minton, Steven and Johnston, Mark D and Philips, Andrew B and Laird, Philip, 1992).

A similar approach, used in the BLACKBOX ² system, involves translating the planning graph into a CNF formula and then using a SAT solver to extract a plan. This method generally performs better than SATPLAN likely because the planning graph has already filtered out many impossible states and actions. It also tends to outperform GRAPHPLAN, most probably because SAT-based methods such as WALKSAT (Kautz, Henry and Selman, Bart and McAllester, David, 2004) offer more flexibility than the more rigid backtracking search used by GRAPHPLAN.

Planning frameworks like GRAPHPLAN, SATPLAN, and BLACKBOX have significantly advanced the discipline of automated planning. Not only have these planners enhanced the overall efficiency and capability of planning systems, but they have also contributed to a deeper understanding of the representational and combinatorial complexities inherent in this area. Nevertheless, these approaches are fundamentally based on propositional logic, which places certain restrictions on the variety of domains they can adequately model. For the field to progress further, it appears increasingly necessary to adopt first-order representations and algorithms, despite the ongoing utility of structures such as planning graphs for generating valuable heuristics.