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].
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 | |