SAT-encoded Logistics Planning Problems

In the logistics planning domain, packages have to be moved between different locations in different cities. Within cities, packages are carried by trucks while between cities they are flown in planes. Both, trucks and airplanes are of limited capacity. The problem involves 3 operators (load, unload, move) and two state predicates (in,at). The initial and goal state specify locations for all packages, trucks, and planes; the plans allow multiple actions to be executed simultaneously, as long as no conflicts arise from their preconditions and effects. Like in the Blocks World Plannig problem, there is an optimisation and a decition variant of the Logistics Planning problem: In the optimisation variant, the goal is to find a shortest plan, whereas in the decision variant, the question is to decide whether a plan of a given length exists. Again, the two variants are tightly related, as shortest plans can be found by solving a series of decision problems. SAT-based approaches to Logistics Planning typically focus on the decision variant.

SAT encoding of Logistics Planning instances

A state-based encoding strategy was used for translating Logistics instances into CNF formulae. In this encoding, only the state predicates are explicitely represented by propositional variables, whereas the operators are only implicitly represented by constraints on transitions of the state predicates.

The SAT encoding used for generating the benchmark problems relies critically on two important techniques for reducing the size of the CNF formulae: operator splitting [KMS96] and simple propositional reductions (unit propagation and subsumption). Operator splitting replaces a predicate which take three or more arguments by a number of binary predicates. This reduces the number of propositional variables for the given problem from O(kn^3) to O(kn^2) where n is the number of blocks and k the number of plan steps. Unit propagation and subsumptions, two well-known propositional reduction strategies, are used to simplify the formulae before applying stochastic local search. These reducations can be computed in polynomial time and eliminate a number of propositional variables thus efficiently reducing the search space. Intuitively, these by applying these strategies the initial and goal states are propagated into the planning structure. Details on the SAT encoding used to generate the benchmark problems can be found in [KS96,KMS96].

The benchmark instances

Our benchmark set contains 7 blocks world planning instances taken from Henry Kautz' and Bart Selman's SATPLAN distribution. These instances are described in Table 1; despite their size they seem to be easier than the Blocks World Planning instances for local search methods.

instance packages (parallel) plan steps vars clauses
logistics.a 8 11 828 6,718
logistics.b 5 13 843 7,301
logistics.c 7 13 1,141 10,719
logistics.d 9 14 4,713 21,991

Table 1: SAT-encoded Logistics Planning instances, contributed by Henry Kautz and Bart Selman (all instances are satisfiable).


[KS96] Henry Kautz and Bart Selman Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search. Proc. AAAI-96, pages 1194--1201, 1996
[KMS96] Henry Kautz and David McAllester and Bart Selman Encoding Plans in Propositional Logic. Proc. KR-96, pages 374--384, 1996