Automatic SAT-Compilation of Planning Problems

1 Introduction

Despite the early formulation of planning as theorem prov·· ing [Green, 1969], most researchers have long assumed that special-purpose planning algorithms are necessary for practi­ cal performance. However, recent improvements in the per­ formance of propositional satisfiability methods [Cook and Mitchell, 1997] cast doubt on this conclusion. Initial results for compiling bounded-length planning problems to SAT were unremarkable [Kautz and Selman, 1992], but recent experi­ ments [Kautz and Selman, 1996] suggest that compilation to SAT might yield the world's fastest STRIPS-style planner.

However, several open questions must be answered before concluding that SAT-based planning dominates specialized algorithms. The experiments of [Kautz and Selman, 1996] used hand-crafted SAT encodings, and while [Kautz et al., 1996] describe methods for compilation, no one has reported experiments on automatically compiled problems and no one knows which en~odings are best. The encodings used by [Kautz and Selman, 1996] included domain information that is inexpressible in the STRIPS action language (e.g., the flu­ ent On is irreflexive and noncommutative) ; to what extent is this information responsible for the speedup they observed? This paper addresses these issues:

*This research was funded in part by Office of Naval Research Grant N00014-94-1-0060, by National Science Foundation Grant !Rl-9303461 , by ARPA/ Rome Labs grant F30602-95-1-0024, and by a gift from Rockwell International Palo Alto Research.

• We present an analytic framework that accounts for all previously reported non-causal encodings, 1 including several novel possibilities. We parameterize the space of encodings along two major dimensions , action and frame representation. For twelve points in this two­ dimensional space, we list the axioms necessary for a minimal encoding, and we calculate the asymptotic en­ coding sizes.
• We describe an automatic compiler that generates all of these encodings. While it is difficult for a compiler to produce encodings that are as lean as the hand-coded versions of [Kautz and Selman, 1996], we describe type­ analysis and factoring techniques that get us close. Ex­ periments demonstrate these methods can reduce the riumber of variables by half and formula size by 80%.
• We run the compiler on a suite of STRIPS-style planning problems, determining that the regular and simply-split explanatory encodings are smallest and can be solved fastest .

2 The Space of Encodings

This section presents a framework that describes all of the AT&T encodings (except for the causal encodings) as well as some new alternatives. Previous work has described indi­ vidual encodings in a variety of ways (e .g., "direct," "state­ based," etc.), but we avoid these terms. Instead we present a parameterized space with two dimensions:

• The choice of a regular, simply split, overloaded split, or bitwise action representation specifies the correspon­ dence between propositional variables and ground (fully­ instantiated) plan actions. These choices represent dif­ ferent points in the tradeoff between the number of vari­ ables and the number of clauses in the formula.
• The choice of classical or explanatory frame axioms varies the way that stationary fluents are constrained.

Our encodings use a standard fluent model in which time takes nonnegative integer values. State-fluents occur at even­ numbered times and actions at odd times. All of the encod­ ings use the following set of universal axioms:

!NIT The initial state is completely specified at time zero, including all properties presumed false by the closed­ world assumption.

GOAL In order to test for a plan of length n, all desired goal properties are asserted to be true at time 2n.

1 The omitted "state-based" encodings can be obtained by re­ solving away the actions in our encodings [Kautz et al. , 1996] .

A:::}P ,E Actions imply their preconditions and effects. For each odd time t between 1 and 2n - 1 and for each con­ sistent ground action, an axiom asserts that execution of the action at time t implies that its effects hold at t + 1 and its preconditions hold at t - 1. For example, suppose that the initial conditions specify four blocks A, B, C, and D. The STRIPS operator of Figure 1 is in­ consistent when instantiated with o = A and s = A, but with o = A, s = B, and d = C it yields the axioms shown, and analogous axioms for preconditions.

2.1 Action Representation

The first major encoding choice is whether to represent ac­ tions as regular, simply split, overloaded split, or bitwise. In the regular representation, each ground action is rep­ resented by a different logical variable, for a total of A = njOpsjiDomjA· such variables (Figure 2 defines these sym­ bols). Since systematic solvers take time exponential in the number of variables, and large numbers of variables also slow stochastic solvers, we would like to reduce this number.

In order to do this, [Kautz and Selman, 1996] introduced simple operator splitting, which replaces each n-ary ac­ tion fluent with n unary fluents throughout the encoding. For example, Move (A, B, C, t) is replaced with the conjunction of MoveArg1(A, t), MoveArg2 (B, t), MoveArg3(C, t). Doing this for all fully-instantiated actions reduces the number of vari­ ables needed to represent all actions to njOpsiiDomjA ·.

In simple splitting, only instances of the same opera­ tor share propositional variables. An alternative is over­ loaded splitting, whereby all operators share the same split fluents . Overloaded splitting replaces Move (A ,B, C, t) by the conjunction of Act(Move,t), Arg1(A,t), Arg2(B,t), Arg3(C,t), while a different action Paint(A,Red,t) is re­ placed with Act(Paint,t), Arg1(A,t), Arg2(Red,t). This technique further reduces the number of variables needed to represent all actions to n(jOpsj + IDomjA.).

The bitwise representation shrinks the number of vari­ ables even more, by representing the actions with only flog2 Al propositional symbols (per odd time step), each representing a bit. The ground actions are numbered . from 0 to A - 1. The number encoded by the bit symbols determines the ground action which executes at each odd time step. For instance, if there were four ground actions, then (·bit1(t) 1\ ·bit2(t)) would replace the first action, (·bit1(t) 1\ bit2(t)) would replace the second, and so forth .

2.2 Frame Axioms

FRAME Classical or explanatory frame axioms constrain un­ affected fluents when an action occurs.

Classical frame axioms [McCarthy and Hayes, 1969] state what fluents are left unchanged by a given action. For ex­ ample, one classical frame axiom for the Move operator in Figure 1 would say "Moving block A from B to C leaves D's clearness unchanged," e.g.,

Adding classical frame axioms for each action and each odd time t to the universal axioms almost produces a valid encoding of the planning problem. However, if no action occurs at timet, the axioms of the encoding can infer nothing about the truth value of fluents at time t + 1, which can therefore take on arbitrary values. The solution is to add AT-LEAST-ONE axioms for each time step.

Move(o,s, d)

PRECOND:

EFFECT :

Block(o) A Clear(o)A

(Table (d) V Clear(d) )A

On(o, s) A of sAo f d As f d

Clear(s) A ·On(o, s)A

·Clear(d) A On(o, d)

Move(A,B,C,t) => Clear(B,t+1)

Move(A,B,C,t) => ·On(A,B,t+1)

Move(A,B,C,t) => ·Clear(C,t+l)

Move(A,B,C,t) => On(A,C,t+1)

Figure 1: Top: STRIPS definition of a blocks-world operator for moving an object from a source to a destination. Bottom: Axiom schema showing an instance of Move implies its effects.

lOps I number of operators

IPredl number of predicate symbols

IIJoml number of constants in the domain

n number of odd time steps in plan (may be < plan length)

Ap max arity of predicates

Ao max arity of operators

Ar length of action representation (predicate symbols per action): regular = 1; simple split = A0 ; overloaded split = Ao + 1; bitwise = pog 2 Al

A = IOpsiiiJomiAo number of ground actions

.r = IPrediiiJomiAp number of ground ftuents

Po

= O(F) max num·fluents mentioned in operator

Figure 2: Symbols used in complexity analyses.

AT-LEAST-ONE A disjunction of every possible fully· instantiated action ensures that some action occurs at each odd time step. (A no-op action is inserted as a pre­ processing step.) Note that action representation has a huge effect on the size of these axioms (Figure 3)?

The resulting plan consists of a totally-ordered sequence of actions; indeed it corresponds roughly to a "linear" encoding in [Kautz et al., 1996], except that they include exclusion ax· ioms (see below) to ensure that at most one action is active at a time. However, exclusion axioms are unnecessary be­ cause the classical FRAME axioms combined with the A:::}P,E axioms ensure that any two actions occurring at time t lead to an identical world-state at time t + 1. Therefore, if more than one action does occur in a time step, then either one can be selected to form a valid plan.

Explanatory frame axioms [Haas, 1987] enumerate the set of actions that could have occurred in order to account for a state change. For example, an explanatory frame ax· iom would say which actions could have caused D's clearness status to change from true to false.

As a supplement to the universal axioms, explanatory frame axioms must be added for each ground fluent and each odd time t to produce a reasonable encoding. With explanatory frames, a change in a fluent's truth value implies that some action occurs, so ( contrapositively) if no action oc­ curs at a time step, this will be correctly treated as a no-op. Therefore, no AT-LEAST-ONE axioms are required.

Since explanatory frames do not explicitly force the fluenll not affected by an executing action to 'remain unchanged, they permit parallelism. Specifically, any actions whose pre­ conditions are satisfied at time t and whose effects do not contradict each other might be executed in parallel. This kind of parallelism is problematic because it can create valid plans which have no linear solution. For example, suppose action a has precondition X and effect Y, while action (3 has precondition --. Y and effect -.X. While these actions might be executed in parallel (because their effects are not contradic­ tory) there is no legal total ordering of the two actions, which is problematic for non-instantaneous real-world actions.

2 AT-LEAST-ONE axioms are not necessary if the bitwise actioa representation is used, bl',cause all spare bit patterns can be used to refer to actual ground actions.

EXCLUSION Linearizability of resulting plans is guaranteed by restricting which actions may occur simultaneously.

Two kinds of exclusion enforce different constraints in the resulti11g plan:

• Complete exclusion: For each odd time step, and for all distinct, fully-instantiated action pairs a, (3, add clauses of the form -.at V --.f3t. Complete exclusion ensures that only one action occurs at each time step, guaranteeing a totally-ordered plan.
• Conflict exclusion: For each odd time step, and for all distinct , fully-instantiated, conflicting action pairs a, (3 , add clauses of the form -.at V --.f3t . In our frame­ work, two actions conflict if one's precondition is incon­ sistent with the other's effect . 3 Conflict exclusion results in plans whose actions form a partial order. Any total order consistent with the partial order is a valid plan.

Because we wish to consider the minimal encoding corre­ sponding to each choice of action and frame representations, we will assume that c;onflict exclusion is used whenever possi­ ble. Conflict exclusion cannot be exploited when using a split action representation, because splitting causes there not to be a unique variable for each fully-instantiated action. For ex­ ample, with simple splitting, it would be impossible to· have two instantiations of the same operator execute at the same time, because their split fluents would interfere. Overloaded splitting further disallows two instantiations of different op­ erators to execute at the same time.

The bitwise action representation requires no action EX­ CLUSION axioms. At any time step, only one fully­ instantiated action's index can be represented by the bit sym­ bols, so a total ordering is guaranteed.

3Contrast our definition of conflict with that of Graph­ plan [Blum and Furst, 1995) and [Kautz and Selman, 1996) . Unlike Kautz and Selman's parallel encoding, but like their linear one, our encodings have axioms stating that actions imply their effects; their parallel encoding prohibits effect-effect conflicts instead.

3 Optimizing Axioms with Factoring

Eight base encodings are generated by choosing among the regular, simple split, overloaded split, and bitwise action representations and choosing either classical or explanatory frames . Unfortunately, choices that lead to a small number of variables (i.e. , the splitting strategies and bitwise) tend to explode the number of clauses or size of each clause. Con­ sider the AT-LEAST-ONE axiom, which is a disjunction of all fully-instantiated actions. Substituting a conjunction of split or bitwise variables for each regular action literal produces a disjunctive normal form formula which blows up exponen­ tially when converted to conjunctive normal form. With sim­ ple ~litting, this axiom grows 4 from n clauses of size A to nAo clauses of size A (see Figure 3).

The formula blowup results from blindly substituting a complete conjunction of split variables for each action in the A=>P,E, FRAME, AT-LEAST-ONE, and EXCLUSION axioms. Fac­ toring can dramatically reduce both the number of clauses and their sizes for simple and overloaded splitting. The idea is to use only a subset of the full conjunction for an ac­ tion whenever possible. Such a partially-instantiated action represents the set of all fully-instantiated actions consistent with it . The bitwise action representation does not admit an easy method of factoring because partial conjunctions of the bit variables are not useful unless a clever action numbering scheme is created.

3.1 Factoring A=>P,E and FRAME Axioms

The A=>P,E and FRAME axioms, which relate a single fluent to a single action, can make good use of partial action in­ stantiations. For example, Figure 1 shows the Move operator and some of the A=>P,E axioms for one possible instantiation of the operator. Ordinary simple splitting will transform the first axiom at the bottom of Figure 1 into

A similar axiom is generated for all pairs of constants s and d for which Move(s,B,d,t) is a consistent action. Since two of the argument values are irrelevant for this axiom, the simpler axiom KoveArg2(B,t) => Clear(B,t+1) can be used instead, eliminating the need to explicitly consider alliLJoml 2 values for KoveArg1 and KoveArg3.

4 The number of logically independent clauses may be substan­ tially smaller than this worst-case bound which results from naive conversion: some clauses may contain duplicated literals, and some clauses 'may logically imply others. Our implementation eliminates these unnecessary literals and clauses.

Factoring A=>P ,E axioms relies on this idea: when relating an action to a fluent, we need only include the parts of the action conjunct pertaining to the arguments that appear in the affected fluent.

The technique extends easily to both classical and ex­ planatory FRAME axioms. Consider the classical frame example given in Section 2.2. Instead of naively split­ ting Move (A, B, C, t) into MoveArgl(A, t) 1\ MoveArg2 (B, t) 1\ MoveArg3 ( C, t) , we observe that the source and object of the Move are irrelevant and generate

Clear(D,t-1) /\MoveArg3(C,t) => Clear(D,t+l)

This formula implicitly represents the set of all classical frame axioms relating the clearness of D to any Move action having C as its destination argument.

Note that while the factoring optimization is crucial in practice (see Section 5.5) , it is equivalent to ordinary splitting in the worst case. In particular, when the arity of precondi­ tion and effect fluents is equal to the arity of the operator, no factoring is possible.

3.2 Factoring EXCLUSION Axioms

Since pairwise exclusion clauses relate actions to other actions (e .g., -.Move(A,B,C,t) V-.Move(A,B,D,t)) instead of relating actions to fluents , the previous technique cannot be used. Instead, we factor these axioms by noting that, rather than excluding whole actions from occurring simultaneously, we can independently exclude the values of each argument to an action.

For example, factored exclusions of the Move operator look like ( -.MoveArgi(a, t) V -.MoveArgi(b, t) ), ranging over all ar­ guments i and distinct constants a and b. This ensures that at most one fully-instantiated Move action is active at time t . By doing this for all operators, we ensure that only one instance of each operator is active at time t.

To complete the exclusion, we need to ensure that no two operators have an active instance at time t . This is accom­ plished by pairwise excluding all possible first arguments of each operator with one another. In other words, we add clauses ( -.aArgl(a, t) V -.,BArgl (b, t)) for all distinct oper­ ators a and ,B and all (not necessarily distinct) constants a and b. Figure 3 shows how factoring reduces the asymptotic number and size of clauses as compared with unfactored split EXCLUSION axioms.

3.3 Factoring AT-LEAST-ONE Axioms

Without factoring, the AT-LEAST-ONE axiom explodes into an exponential morass during the conversion to CNF. For­ tunately, it can be factored very easily, yielding the disjunc­ tion of all possible first arguments to all operators, i.e., an axiom of the form: (Op1Arg1(A,t) V Op1Arg1(B,t) V .. . V Op2Arg1(A,t) V Op2Argl(B,t) V . .. ) . This axiom now re­ quires only n clauses of size IOpslllJoml, quite a reduction from the unfactored case.

3.4 Preventing Partial Action Execution

The previous three subsections show how to factor each part of the encoding. All three parts rely on the ability to refer to parts of an action instead of always referring to a complete instantiation of an action. However, the underlying assump­ tion is that, whenever any part is instantiated, so is the rest of the action.

:For example, we would not want a factored frame clause to have any effect unless a full action implied by that frame was actually being executed at the current time step. Otherwise, the frame could constrain the resulting plan, even though the action referred to by the frame is never fully executed.

NO-PARTIAL We add axioms which state that, whenever any part of an operator is instantiated, so is the rest.

Here are the partial action elimination axioms for the Move operator:

(MoveArgl (A, t) V MoveArgl (B, t) V ... ) {::} (MoveArg2(A,t) VMoveArg2(B,t) V .. . ) (MoveArgl(A, t) V MoveArgl(B, t) V .. . ) {::} (MoveArg3 (A, t) V MoveArg3(B, t) V .. . )

These axioms ensure that whenever any split fluent of Move is true, then some complete instantiation of Move is true. Figure 3 shows the number and size of the resulting clauses.

4 The MEDIC Planner

Following the encodings described above, we have imple­ mented a classical plaimer which accepts traditional 5 inputs (initial state, goal formula, and STRIPS action schemata) and returns a sequence of actions that will achieve the goal. The MEDIC planner operates by compiling the planning prob­ lem into clausal form, solving the SAT problem, and trans­ lating the satisfying truth assignment back into actions. De­ pending on the switch settings, any of the SAT encodings described above can be generated. Thus the MEDIC planner forms a unique testbed for exploring the properties of the different encodings.

The architecture of the planner is shown in Figure 5. Ac­ tion schemata are parsed using the preprocessor from the UCPOP planner [Penberthy and Weld, 1992] and type optithose that can be false) is computed by an iterative dataflow mization (see below) is performed. Next, guided by the choice analysis. The first approximation is the initial condition; at of action and frame representations (Figure 4), the compiler each step any fluents in the effects of actions that can fire, creates a master axiom schema representing all action posgiven the current approximations, are added to the sets. This sibilities for one time step. The periodic axiom schema is process is guaranteed to terminate and is not tantamount to instantiated multiple times, based on the plan length cursolving the planning problem since time is ignored, thereby rently being considered. The output of this duplication modpermitting impossible situations, like the presence of a fluent ule, combined with the initial state and goal specification, and its negation. is simplified by pure literal elimination, unit clause propagation, and duplicate literal elimination using a fast (linear time) procedure [Van Gelder and Tsuji, 1996]. The result- CNF simplification operates without knowledge of the strucing clauses are solved using Walksat [Selman et al., 1996] or Tableau [Crawford and Auton, 1993].

5By contrast, the implementation of [Kautz and Selman, 1996] accepts "direct" encodings in a logical constraint language, rather than STRIPS actions.

4.1 Optimizations

Planning via reduction to propositional satisfiability is im­ practical without a number of optimizations which determine the truth values of fluents or limit the ground instantiations of actions. Foremost among these are type optimizations. A type is a fluent which no action affects.

Types can constrain operator instantiation by ruling out impossible ground versions. For instance, if A and B are the only blocks, we can prune any instantiation of the Move op­ erator (Figure 1) which does not assign o to either A or B. When such preconditions are reflected in the operator instan­ tiations, the types themselves need not appear in the final encoding; for instance, the Block precondition would be re­ moved from Move. This mechanism is a generalization of the obvious one for handling equality and inequality constraints, which are special cases of types.

Because of the usefulness of type information, we have ex­ plored methods of inferring types of arguments when oper­ ators do not specify them. Suppose that Block(o) did not appear in the Move definition in Figure 1, but that when­ ever Clear(o) appears in an action's effect (for any variable o), that action's precondition contains the fluent Block(o) . Then no constant can become Clear without being a Block. If every constant which is Clear in the initial conditions is also a Block, we can deduce that every Clear constant must be a Block and add Block(o) to the Move precondition.

Similarly, inequality constraints can be inferred if a fluent appears both positively and negatively in an operator, since the two bindings cannot be identical. Since the Move operator of Figure 1 has effects ·On(o, s) and On(o, d), the s # d constraint would be inferred if it were not already present.

An operator's instantiations can be further pruned by elim­ inating symmetric operator instantiations. For instance, if an operator a takes two arguments which are used identically, then there is no sense considering both of the bindings a( A, B) and a(B, A) ; we arbitrarily select one of the possibilities. This analysis cuts the number of ground instantiations by about an order of magnitude for the refrigerator domain.

The MEDIC planner further reduces bindings and infers invariant fluents by enforcing a form of consistency. An ap­ proximation to the set of fluents that can be true (and also to The CNF simplification step is also quite important, since it is fast and can reduce the formula size enormously. Though ture of the problem, its effects are similar to some of the optimizations listed above. For instance, it can do much of the type elimination described above. However, performing these steps earlier can reduce encoding time by a factor of four or more due to generation of smaller formulae. Further, these optimizations can often allow the simplifier to reduce a formula more than it otherwise could.

Optimization and Factoring

Factored action representations reduce the benefit of these type optimizations. When performing factored simple split­ ting, only unary types can be eliminated, since their effect is restricted to (and fully reflected by) just one of the newly­ introduced action predicate symbols. Binary types such as # cannot be eliminated: consider a binary operator a which takes two non-equal arguments. Given two objects A and B, only two instantiations a( A, B) and a(B, A) are possible, but since the new action fluents aArg1 and aArg2 can each take either A or B as an argument, it is necessary to leave the ax­ iom aArgl(x) /\aArgl(y) => x #yin the encoding to prevent the illegal argument combinations.

Overloaded action representations do not admit elimina­ tion of even unary types, since a single action fluent rep­ resents the nth argument to many different operators with different constraints.

4.2 Searching for the Minimal Plan

So far we have assumed that one is trying to find a plan of known length, but in general the plan length is not known in advance. The MEDIC planner is capable of both linear and binary search on plan lengths. 6 Our encodings support the linear search strategy without any modification. To imple­ ment binary search for the minimal plan length, we include an explicit no-op (maintain) action when using classical frame axioms. This allows plans longer than the minimal length to succeed.

Because Walksat is stochastic, finding a minimal length plan requires a systematic solver such as Tableau instead of (or in addition to) Walksat . For even moderately-sized prob­ lems, however, Tableau can take an unreasonably long time to verify that no solution exists. (Such verification is moot

6 Because SAT solving time is potentially exponential in encod­ ing size, we conjecture that linear search strategy is better, but we haven't performed serious tests.

*

*

Figure 6: Numbers of variables, clauses, and literals in simplified CNF formulas resulting from each of eight encodings, plus the Satplan hand-encoding (sans domain-specific axioms). Values reported as 10 are actually 0: that is, the CNF simplifier solved the problem. Times less than one tenth second are reported as one tenth.

when trying to find any satisfying plan rather than the short­ est one.)

5 Experiments

To test the various encodings, we encoded a suite of planning problems using each of the eight encodings. Factoring was applied when split action representations were used. Figure 6 plots the number of variables, clauses, and literals in the final simplified CNF formulae.

Figure 6 also reports Walksat solution 7 times (averaged over five runs), but note that timing data is hard to interpret. Walksat is not always the fastest solution method. We used the suggested Walksat flag settings from the Satplan planner , but these flags might favor some encodings over others. The timings reported in [Kautz and Selman, 1996] are each min­ ima over many Walksat runs with varying parameter values. It is believed that solution time correlates with CNF size, but automatically determining which solver flags are best for a particular problem is an open problem [Selman et al., 1997], though progress has been made recently [McAllester et al. , 1997] .

7 We do not report encoding or simplification times, which for medium and large problems are dominated by solution time.

From the asymptotic size bounds of Figure 4 one would expect the bitwise encodings to have the smallest number of variables and the regular encodings to have the largest number of variables. Surprisingly, neither expectation was fulfilled.

5.1 The Smallest Encodings

The two smallest encodings are the regular and simply split explanatory encodings, and these encodings had quick solve times as well. These successes bring to light several interest­ ing points about the relative merits of the encodings.

First , it is clear that explanatory frame clauses are superior to classical frame clauses. Explanatory frames are smaller because they only state what changes, rather than what does not change, when an action occurs. In general, we expect each action to affect relatively few fluents .

Parallelism is also a big advantage (as shown by the success of the regular explanatory encoding) . Since parallel plans have shorter length, the formula contains fewer copies of the periodic axioms. Additionally, conflict exclusion axioms are a subset of complete exclusions, which prohibit all pairs of actions. Conflict exclusion only excludes pairs of actions that would not be otherwise excluded but should be in order to guarantee the existence of a linearization of the partial order plan returned.

It is quite surprising that the regular explanatory encod­ ing has so few variables. [Kautz and Selman, 1996] dismiss this encoding as impractical. While its size can blow up pro­ hibitively in the worst case (see Figure 4), in practice the encoding maintains excellent variable and clause sizes. And it remains competitive even as problems increase in size (e.g., problem sequence logO, log1, ... , logA) . We suspect the com­ piler's type optimizations (which are handicapped by factored splitting) deserve the credit .

5.2 The Largest Encodings

The two worst encodings are the regular and bitwise classi­ cal encodings. We have already mentioned the superiority of explanatory to classical frames. Regular classical is out­ performed by the two split classical encodings. Worst-case splitting clause sizes can be much bigger than the regular encoding, but in practice factoring seems to keep the sizes competitive. Splitting also may provide the simplifier with more flexibility, allowing it to deduce more, because it can reason about parts of actions instead of only about fully­ instantiated actions without hope of generalizing. Finally, these encodings are also aided by the great decrease in the number of variables as compared with the regular encoding.

On the other hand, the bitwise encoding, which has the smallest number of variables before simplification, is the worst encoding of all. Simplification is relatively ineffective on this encoding, as other encodings have fewer variables af­ ter the simplification phase. This may be related to the fact that bitwise uses one set of variables to encode all possible actions in the domain, thereby making it next to impossible for the simplifier to reason about the truth values of these variables. Finally, the graph of number of literals points to the obvious blow-up that bitwise incurs in exchange for the small variable size.

5.3 Comparison with Satplan

Although our encodings cannot be expected to be as compact as the hand-made Satplan encodings, our best encodings are surprisingly competitive. The first seven problems of Fig­ ure 6 include a ranking for the Sat plan direct encoding of the problem, from which domain-specific axioms (see Section 5.6) have been removed for purposes of comparison. Our best en­ codings actually outperform the Satplan encodings on two of the smaller problems, as the simplification process is able to satisfy our forinulas completely. As the problems get larger, the Satplan encodings begin to dominate. However, our best automatic encoding appears to be always within a factor of two of the Satplan size.

5.4 Type Optimizations

Type optimizations can substantially reduce formula size: Figure 7 compares formula sizes with and without these op­ timizations. These numbers understate the benefits of the optimizations, because they do not include data for prob­ lemsthat were too large to solve without type optimizations but could be solved with them. The optimizations are criti­ cal for the classical encodings, cutting their size by about two thirds. However, these optimizations are much less effective on explanatory encodings. In fact, the optimizations appear to be superfluous for the regular explanatory encoding: the CNF simplifier obtains all of the type optimization benefits without considering the structure of the problem, using only the resulting formula.

These contrasts may be attributable to the way in which the simplifier interacts with the various encodings. Classi­ cal encodings are much more constraining than explanatory encodings, because they explicitly enforce all truth values at time t + 1 when an action occurs at timet. This rigidity may make it hard for the simplifier to reduce the encoding size, thereby relying more heavily on the type optimizations to make deductions about the encoding. The regular explana­ tory encoding, which uses conflict exclusion, is the most flex­ ible of all of the encodings. Therefore, it seems that any static optimizations that we make are easily teased out of the encoding by the simplifier.

5.5 Factoring

Figure 8 shows that factoring makes a big difference com­ pared with unfactored splitting. While factoring does not reduce variable size at all in the base encoding, it does lead to small drops in variable size after simplification. Factoring's big effects, however, are in clause and (especially) literal size. This is important, because this reduction is precisely the rea­ son that we introduced the idea of factoring. Although in the worst case, factoring has no effect, it is clear that factoring is critical in practice.

5.6 Domain Specific Axioms

The "direct" encodings of [Kautz and Selman, 1996] pro­ vide hand-coded, domain-specific information which is im­ possible to specify in terms of STRIPS actions but is natural when writing general logical axioms. For example, in their blocks world problems Kautz et al. state that the relation On is both non-commutative and irreflexive, only one block may be on another at any time, every block is on exactly one other object, blocks can't be both clear and have something on them, and the Table is never on anything. To determine how much (if at all) this additional information affected the planning problem, we removed these domain-specific axioms from the AT&T encodings and compared the size and speed of the resulting SAT problems. As Figure 9 shows, eliminat­ ing the axioms decreased the number of clauses, but increased the number of variables (presumably because unit-clause and pure-literal simplification was less effective) . Without the domain-dependent axioms, the planning problems took sub­ stantially longer. These results suggest it would be useful to investigate whether a compiler could deduce some of these axioms automatically. We believe our type optimizations to be a good start at achieving this goal .

6 Conclusions

This paper makes several contributions:

• We develop a simple framework that generates eight ma­ jor encodings, which account for all of the non-causal AT&T encodings as well as several novel ones. In par­ ticular, the introduction of overloaded splitting and the bitwise representation, combined with the regular and simply-split encodings, creates a spectrum of choices highlighting the tradeoff between variable and clause sizes.
• We describe an automatic compiler that takes classical STRIPS planning problems and generates SAT prob­ lems using all of the above encodings. Our compiler includes many interesting features, including a type in­ ference and optimization mechanism.
• We use the compiler to perform an empirical analysis of tradeoffs in the space of encodings. We show that explanatory frames and conflict exclusion are dominant, and regular acton representation is surprisingly effective.

Many exciting problems remain. Clearly we need to bet­ ter investigate the solve-time characteristics of the encod­ ings. Automatically generating domain-specific axioms , such as those in Section 5.6, is a promising direction. We also hope to investigate additional type inference methods. There are also many hybrid encodings which would be interesting to explore. Allowing inter-operator parallelism in the simply­ split explanatory encoding could take advantage of both of the best encodings. (As mentioned earlier, simple splitting prevents the possibility of parallel instantiations of the same operator, as their split variables will interfere.) Another hy­ brid option is the addition of "action" variables, similar to those of overloaded splitting, to the simple splitting encod­ ing. These extra variables can greatly compact many parts of a factored split encoding. A third hybrid would use bitwise representations for the split fluents of simple or overloaded split actions, avoiding the disadvantages of the bitwise ac­ tion representation while reducing the number of variables. One can also imagine compiling part of a domain theory with one encoding and using a different encoding for other parts. Finally, it would be interesting to automate the AT&T state­ based encodings and to integrate their causal encodings into our framework.

7 Acknowledgments

Jared Saia, Nick Kushmerick, and Marc Friedman con­ tributed to our implementation and testing framework. David Smith made many insightful observations that led to a major reformulation of our encoding space. Bart Selman, David McAllester, and Henry Kautz engaged in helpful dis­ cussions and kindly provided their Satplan code. Jimi Craw­ ford provided Tableau code.