Understanding Planning Formalisms
Artificial Intelligence: A Modern Approach - Chapter 11
Table of Contents
1. The language of planning problems
1.1. Representation of states
Planners decompose the world into logical conditions and represent a state as conjunction of positive litereals. 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,Melbourne) \land At(Plane_2,Sydney)\) might represent a state in the package delivery problem.
Literals in first-order state descriptions must be ground and function-free. Literals such as \(At(x,y)\) or \(At(Father(Fred),Sydney)\) are not allowed. The closed-world assumption is used, meaning that any conditions that are not mentioned in a state are assumed false.
1.2. Representation of goals
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\) 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\).
1.3. Representation of actions
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:
1.4. Expressiveness and extensions
The various restrictions imposed by the STRIPS representation were chosen in the hope of making planning algorithms simpler and more efficient, without making it too difficult to describe real problems. One of the most important restrictions is that litereals be \(function-free\). With this restriction, we can be sure that any action schema for a given problem can be propositionalized - that is, turned into a finite collection of purely proposition action representations with no variables. For example, in the air cargo domain for a problem with 10 planes and five airports, we could translate the \(Fly(p,from,to)\) schema into \(10 \times 5 \times 5 = 250\) purely propositional actions.
| STRIPS Language | ADL Language |
|---|---|
| Only positive literals in states: \(Poor \land Unknown\) | Positive and negative literals in states: \(\lnot Rich \land \lnot Famous\) |
| Closed World Assumption: Unmentioned literals are false. | Open World Assumption: Unmentioned literals are unknown. |
| Effect \(P \land \lnot Q\) means add \(P\) and delete \(Q\). | Effect \(P \land \lnot Q\) means add \(P\) and \(\lnot Q\) and delete \(\lnot P\) and \(Q\). |
| Only ground literals in goals: \(Rich \land Famous\) | Quantified variables in goals: \(∃xAt (P_1, x) \land At(P_2, x)\) is the goal of having \(P_1\) and \(P_2\) in the same place. |
| Goals are conjunctions: \(Rich \land Famous\) | Goals allow conjunction and disjunction: \(\lnot Poor \land (Famous \lor Smart)\) |
| Effects are conjunctions. | Conditional effects allowed: when \(P\) : \(E\) means \(E\) is an effect only if \(P\) is satisfied. |
| No support for equality. | Equality predicate \((x = y)\) is built in. |
| No support for types. | Variables can have types, as in \((p : Plane)\) |
2. Planning with propositional logic
The approach is based on testing the satisfiability of a logical sentence rather than proving a theorem. We will be finding models of propositional sentences that look like this:
The statement will incorporate proposition symbols for every possible action occurrence. A model that satisfies the statement will assign \(true\) to actions that are part of a valid plan and \(false\) to those that are not. An assignment corresponding to an invalid plan will not be considered a model, as it will contradict the assertion that the goal is achievable. If the planning problem is unsolvable, the statement will be regarded as unsatisfiable.
2.1. Describing planning problems in propositional logic
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, consider 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 algorithm's termination, an arbitrary upper limit, \(T_\text{max}\), is established. This algorithm is illustrated in the following pseudo-code.
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 \(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 knowledge base \(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\).