clear and on are state predicates, while move is an action predicate. The axioms which specify the problem can be grouped into 4 categories:
The last group of actions is redundant, but has been found to be useful for speeding up local search. For a given blocks world planning instance, instantiating the predicates listed above gives the propositional variables over which the axioms can then be formulated as CNF clauses.
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 the reductions mentioned above, they are still very large when compared to other instances of our benchmark suit. bw_large.c and bw_large.d belong to the hardest problems which can be solved by state-of-the-art SAT algorithms in reasonable time.
instance | blocks | steps | vars | clauses |
anomaly | 3 | 3 | 48 | 261 |
medium | 5 | 4 | 116 | 953 |
bw_large.a | 9 | 6 | 459 | 4,675 |
huge | 9 | 6 | 459 | 7,054 |
bw_large.b | 11 | 9 | 1,087 | 13,772 |
bw_large.c | 15 | 14 | 3,016 | 50,457 |
bw_large.d | 19 | 18 | 6,325 | 131,973 |
Table 1: SAT-encoded Blocks World Planning instances (linear encoding), 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 |