SAT-encoded Blocks World Planning Problems

The Blocks World is a very well-known problem domain in AI research. The general scenario in Blocks World Planning comprises a number of blocks and a table. The blocks can be piled onto each other, where the downmost block of a pile is always on the table. For the benchmark problems, taken from [KS96], there is only one operator which moves the top block of a pile to the top of another pile or onto the table. Given an initial and a goal configuration of blocks, the problem is to find a sequence of operators which, when applied to the initial configuration, leads to the goal situation. Such a sequence is called a (linear) plan. Blocks can only be moved when they are clear, i.e., no other block is piled on top of them, and they can be only moved on top of blocks which are clear or onto the table. If these conditions are satisfied, the move operator always succeeds. There is an optimisation and a decision variant of the Blocks World 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. The two variants are tightly related, as shortest plans can be found by solving a series of decision problems. SAT-based approaches to Blocks World Planning typically focus on the decision variant.

SAT encoding

A linear encoding strategy was used for translating Blocks World instances into CNF formulae. The encoding is based on the following predicates:

clear(x,t) - block x is clear at time t
on(x,y,t) - block x is directly on top of y at time t
move(x,y,z,t) - block x is moved from block y on block z at time t

clear and on are state predicates, while move is an action predicate. The axioms which specify the problem can be grouped into 4 categories:

actions imply their preconditions and effects,
exactly one action can be executed at each time t,
classical frame conditions which state that state predicates do not change between t and t+1 if they are not directly affected by the action at time t,
in move(x,y,z,t), x,y, and z are distinct.

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

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

Bibliography

[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

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