The LPSAT Engine & Its Application to Resource Planning

1 Introduction

Recent advances in satisfiability (SAT) solving technol­ ogy have rendered large, previously intractable prob­ lems quickly solvable [Crawford and Auton, 1993; Sel­ man et al., 1996; Cook and Mitchell, 1997; Bayardo and Schrag, 1997; Li and Anbulagan, 1997; Gomes et al., 1998]. SAT solving has become so successful that many other difficult tasks are being compiled into propo­ sitional form to be solved as SAT problems. For ex­ ample, SAT-encoded solutions to graph coloring, plan­ ning, and circuit verification are among the fastest ap­ proaches to these problems [r mtz and Selman, 1996; Selman et al., 1997].

But many real-world tasks have a metric aspect. For instance, resource planning, temporal planning, schedul­ ing, and analog circuit verification problems all require reasoning about real-valued quantities. Unfortunately, metric constraints are difficult to express in SAT en­ codings1. Hence, a solver which could efficiently han­ dle both metric constraints and propositional formulae would yield a powerful substrate for handling AI prob­ lems.

*We thank people who provided code, help, and discus­ sion: Greg Badros, Alan Borning, Carin Anderson, Mike Ernst, Zack Ives, Subbarao Kambhampati, Henry Kautz, Jana Koehler, Tessa Lau, Denise Pinnel, Rachel Pottinger, Bart Selman, and the blind reviewers. This research was funded in part by Office of Naval Research Grant N0001498-1-0147, by the ARCS foundation Barbara and Tom Ca­ ble fellowship, by National Science Foundation Grants IRI9303461 and IIS-9872128, and by a National Science Foun­ dation Graduate Fellowship.

This paper introduces a new problem formulation, LCNF, which combines the expressive power of proposi­ tional logic with that of linear equalities and inequalities. We argue that LCNF provides an ideal target language into which a compiler might translate tasks that combine logical and metric reasoning. We also describe the LPSAT LCNF solver, a systematic satisfiability solver integrated with an incremental Simplex algorithm. As LPSAT ex­ plores the propositional search space it updates the set of metric requirements managed by the linear program solver; in turn, Simplex notifies the propositional solver if these requirements become unsatisfiable.

We report on three optimizations to LPSAT: learn­ ing and backjumping, adapting LPSAT's core heuristic to trigger variables, and using random restarts. The most effective of these is the combination of learning and back­ jumping; LPSAT learns new clauses by discovering expla­ nations for failure when a branch of its search terminates. The resulting clauses guide backjumping and constrain future truth assignments. In particular, we show that analysis of the state of the linear program solver is cru­ cial in order to learn effectively from constraint conflicts.

To demonstrate the utility of the LCNF approach, we also present a fully implemented compiler for resource planning problems. Figure 1 shows how the components fit together. Their performance is impressive: LPSAT solves large resource planning problems (encoded in a variant of the PDDL language [McDermott, 1998] based on the metric constructs used by metric IPP [Koehler, 1998]) , including a metric version of the ATT Logistics domain [Kautz and Selman, 1996].

1 Encoding each value as a separate boolean variable is a simple but unwieldy solution; bitwise-encodings pro­ duce smaller formulae but ones which appear very hard to solve [Ernst et al., 1997].

2 The LCNF Formalism

The LCNF representation combines a propositional logic formula with a set of metric constraints. The key to the encoding is the simple but expressive concept of trig­ gers - each propositional variable may "trigger" a con­ straint ; this constraint is then enforced whenever the trigger variable's truth assignment is true.

Formally, an LCNF problem is a five-tuple (R, V, 6. , 1::, T) in which R is a set of real-valued variables, V is a set of propositional variables, 6. is a set of linear equality and inequality constraints over variables in R, 1:: is a propositional formula in CNF over variables in V , and T is a function from V to 6. which establishes the constraint triggered by each propositional variable. We require that 6. contain a special null constraint which is vacuously true, and this is used as the T-value for a variable in V to denote that it triggers no constraint. Moreover, for each variable v we define T( · V) = null.

Under this definition, an assignment to an LCNF prob­ lem is a mapping, cp, from the variables in R to real val­ ues and from the variables in V to truth values. Given an LCNF problem and an assignment, the set of active constraints is {c E 6.I:Jv E V cp(v) =true 1\ T(v) = c}. We say that an assignment satisfies the LCNF problem if and only if it makes at least one literal true in each clause of 1:: and satisfies the set of active constraints.

Figure 2shows a fragment of a sample LCNF problem: a t ruck, which carries a maximum load of 30 and fuel level of 15, can make a Delivery by executing the Move action. We discuss later why it cannot have a GoodTrip.

3 The LPSAT Solver

Our first step in constructing the LPSAT engine was to choose solvers to use as the foundation for its metric and propositional solving portions. The choice was mo­ tivated by the following criteria:

1. It must be easy to modify the propositional solver in order to support triggers and handle reports of inconsistency from the constraint reasoner.
2. The metric solver must support incremental modi­ fications to the constraint set.
3. Because a Simplex solve is more expensive than setting a single propositional variable's value, the propositional solver should minimize modifications to the constraint set.

These principles led us to implement the LPSAT en­ gine by modifying the RELSAT satisfiability engine [Ba­ yardo and Schrag, 1997] and combining it with the CASSOWARY constraint solver [Borning et al., 1997; Badros and Borning, 1998] using the method described in [Nelson and Oppen, 1979]. RELSAT makes an excellent start for processing LCNF for three reasons. First, it per­ forms a systematic, depth-first search through the space of partial truth assignments; this minimizes changes to the set of active metric constraints. Second, the code is exceptional!y well-structured. Third, RELSAT incor­ porates powerful learning and backjumping optimiza­ tions. CASSOWARY is an appropriate Simplex solver for handling LCNF because it was designed to support and quickly respond to small changes in its constraint set.

In order to build LPSAT, we modified RELSAT to in­ clude trigger variables and constraints. This required four changes. First, the solver must trigger constraints as the truth assignment changes. Second, the solver must now check for a solvable constraint set to ensure that a truth assignment is satisfying. Third, the solver must report in its solution not only a truth assignment to the boolean variables, but an assignment of real values to the constraint variables 2 . Finally, since even a purely posi­ tive trigger variable may (if set to true) trigger an incon­ sistent constraint, pure literal elimination cannot act on positive trigger variables 3 . Figure 3 displays pseudocode for the resulting algorithm.

4 Incorporating Learning and Backjumping

LPSAT inherits methods for learning and backjumping from RELSAT [Bayardo and Schrag, 1997]. LPSAT's depth-first search of the propositional search space cre­ ates a partial assignment to the boolean variables. When the search fails , it is because the partial assignment is inconsistent with the LCNF problem. LPSAT iden­ tifies an inconsistent subset of the truth assignments in the partial assignment, a conflict set, and uses this subset to learn in two ways. First, since making the truth assignments represented in the conflict set leads inevitably to failure, LPSAT can learn a clause disal­ lowing those particular assignments. For example, in the problem from Figure 2 the constraints triggered by setting MinFuel, MaxFuel, MaxLoad, and AllLoaded to true are inconsistent, and MinFuel, MaxFuel, and Al­ lLoaded form a conflict set. So, LPSAT can learn the clause (-.MinFuel V -.MaxFuel V -.AllLoaded) . Second, because continuing the search is futile until at least one of the variables in the conflict set has its truth assign­ ment changed, LPSAT can backjump in its search to the deepest branch points at which a conflict set variable re­ ceived its assignment, ignoring any deeper branch points. Figure 4 shows a search tree in which MinFuel, MaxFuel, MaxLoad, and AllLoaded have all been set to true. Using the conflict set containing MinFuel, MaxFuel, and All­ Loaded, LPSAT can backjump past the branchpoint for MaxLoad to the branchpoint for MinFuel, the deepest member of the conflict set which is a branchpoint.

2 While the assignment to the constraint variables is opti­ mal according to CASSOWARY's objective function , it is not guaranteed to be the globally optimal assignment to the real variables by the same measure; a different assignment to the propositional variables might provide a better solution. So, the specific function used is not vital (we use CASSOWARY's default which minimizes the slack in inequalities) .

3 This restriction falls in line with the pure literal elim­ ination rule if we consider the triggers themselves to be clauses. The trigger MaxLoad => (load ::; 30) from Fig­ ure 2 would then become the clause ·MaxLoad V (load ::; 30) , and MaxLoad could no longer be purely positive.

However, while LPSAT inherits methods to use con­ flict sets from RELSAT, LPSAT must produce those conflict sets for both propositional and constraint failures while RELSAT produces them only for propositional failures. Thus, given a propositional failure LPSAT uses RELSAT's conflict set discovery mechanism unchanged, learning a set based on two of the clauses which led to the con­ tradiction [Bayardo and Schrag, 1997]. For a constraint conflict, however, LPSAT identifies an inconsistent sub­ set of the active constraints, and the propositional trig­ gers for these constraint compose the conflict set. We examine two methods for identifying these inconsistent subsets.

In our first method, called global conflict set discovery, LPSAT includes the entire set of active constraints in the conflict set. This mechanism is simple but often subop­ timal since a smaller conflict set would provide greater pruning action. Indeed, preliminary experiments showed that - while global conflict set discovery did increase solver speed over a solver with no learning or backjump­ ing facility - the conflict sets were on average twice as large as those found for logical conflicts.

In our second method, called minimal conflict set dis­ covery, LPSAT identifies a (potentially) much smaller set of constraints which are responsible for the conflict. Specifically, our technique identifies an inconsistent con­ flict set of which every proper subset is consistent.

Figure 5 illustrates the constraints from the example in Figure 2. The constraints MaxLoad, MaxFuel, and Min­ Fuel and the implicit constraints that fuel and load be non-negative are all consistent; however, with the intro­ duction of the dashed constraint marked AllLoaded the constraint set becomes inconsistent. Informally, LPSAT finds a minimal conflict set by identifying only those con­ straints which are, together, in greatest conflict with the new constraint. We now discuss how LPSAT discovers the conflicting constraints in this figure and which set it discovers.

When LPSAT adds the AllLoaded constraint to CASSOWARY's constraint set, CASSOWARY initially adds a "slack" version of the constraint which allows error and is thus trivially consistent with the current constraint set. This error is then minimized by the same routine used to minimize the overall objective function [Badros and Borning, 1998]. In Figure 5, we show the minimiza­ tion as a move from the initial solution at the upper left corner point to the solution at the upper right cor­ ner point of the shaded region. The error in the solu­ tion is the horizontal distance from the solution point to the new constraint AllLoaded. Since no further progress within the shaded region can be made toward AllLoaded, the error has been minimized; however, since the error is non-zero, the strict constraint is inconsistent.

At this point, LPSAT uses "marker variables" (which CASSOWARY adds to each original constraint) to estab­ lish the conflict set. A marker variable is a variable that was added by exactly one of the original constraints and thus identifies the constraint in any derived equations. LPSAT examines the derived equation that gives the er­ ror for the new constraint, and notes that each constraint with a marker variable in this equation contributes to keeping the error non-zero. Thus, all the constraints identified by this equation, plus the new constraint it­ self, compose a conflict set.

In Figure 5 the MinFuel and MaxFuel constraints re­ strain the solution point from coming closer to the All­ Loaded line. If the entire active constraint set were any two of those three constraints, the intersection of the two constraints' lines would be a valid solution; however, there is no valid solution with all three constraints.

Note that another conflict set (AllLoaded plus MaxLoad) exists with even smaller cardinality than the one we find . In general, there may be many minimal conflict sets, and our conflict discovery technique will discovery only one of these, with no guarantee of discov­ ering the global minimum. Some of these sets may prove to have better pruning action, but we know of no way to find the best minimal conflict set efficiently. How­ ever, the minimal conflict set is at least as good as (and usually better than) any of its supersets.

A brief proof that our technique will return a min­ imal conflict set appears in the longer version of this paper [Wolfman and Weld, 1999].

5 The Resource Planning Application

In order to demonstrate LPSAT's utility, we implemented a compiler for metric planning domains (starting from a base of IPP's [Koehler et al., 1997] and BLACK­ sox's [Kautz and Selman, 1998] parsers) which trans­ lates resource planning problems into LCNF form. Af­ ter LPSAT solves the LCNF problem, a small decoding unit maps the resulting boolean and real-valued assign­ ments into a solution plan (Figure 1) . We believe that this translate/solve/decode architecture is effective for a wide variety of problems.

5.1 Action Language

Our planning problems are specified in an extension of the PDDL language [McDermott, 1998] ; we support PDDL typing, equality, quantified goals and effects, dis­ junctive preconditions, and conditional effects. In ad­ dition, we handle metric values with two new built­ in types: float and fluent. A float's value may not change over the course of a plan, whereas a fluent's value may change from time step to time step. Moreover, we support fluent- and float-valued functions, such as ?distance[Nagoya,Stockholm] .

Floats and fluents are manipulated with three special built-in predicates: test, set, and influence. Test statements are used as predicates in action precondi­ tions; set and influence are used in effects. As its argument, test takes a constraint (an equality or inequality between two expressions composed of floats, fluents, and basic arithmetic operations); it evaluates to true if and only if the constraint holds. Set and influence each take two arguments: the object (a float or fluent) and an expression. If an action causes a set to be asserted, the object's value after the action is defined to be the expres­ sion's value before the action. An asserted influence changes an object's value by the value of the expression, as in the equation object := object + expression; mul­ tiple simultaneous influences are cumulative in their effect [Falkenhainer and Forbus, 1988].

5.2 Plan Encoding

The compiler uses a regular action representation with explanator:y frame axioms and conflict exclusion [Ernst et al., 1997j. We adopt a standard fluent model in which time takes nonnegative integer values. State-fluents oc­ cur at even-numbered times and actions at odd times. The initial state is completely specified at time zero, in­ cluding all properties presumed false by the closed-world assumption.

Each test, set, and influence statement compiles to a propositional variable that triggers the associated constraint. Just as logical preconditions and effects are implied by their associated actions, the triggers for met­ ric preconditions and effects are implied by their actions.

The compiler must generate frame axioms for con­ straint variables as well as for propositional variables, but the axiomatizations are very different. Explanatory frames are used for boolean variables, while for real vari­ ables, compilation proceeds in two steps. First, we create a constraint which, if activated, will set the value of the variable at the next step equal to its current value plus all the influences that might act on it ( untriggered influ­ ences are set to zero). Next, we construct a clause which activates this constraint unless some action actually sets the variable's value.

For a parallel encoding, the compiler must consider certain set and influence statements to be mutually exclusive. For simplicity, we adopt the following con­ vention: two actions are mutually exclusive if and only if at least one sets a variable which the other either influences or sets.

This exclusivity policy results in a plan which is cor­ rect if actions at each step are executed strictly in par­ allel; however, the actions may not be serializable, as demonstrated in Figure 6. In order to make parallel actions arbitrarily serializable, we would have to adopt more restrictive exclusivity conditions and a Jess expres­ sive format for our test statements.

6 Experimental Results

There are currently few available metric planners with which to compare LPSAT. The ZENO system [Penberthy and Weld 1994] is more expressive than our system, but ZENO is ~nable even to complete easy-1, our simplest metric logistics problem. There are onlx a few results available for Koehler's metric IPP system [Koehler, 1998], and code is not yet available for direct comparisons.

In light of this, this section concentrates on displaying results for LPSAT in an interesting domain and on de­ scribing the heuristics and optimization we used to en­ hance LPSAT's performance. We report LPSAT solve time, running on a Pentium II 450 MHz processor with 128MB of RAM, averaged over 20 runs per problem, an~ show­ ing 95 percent confidence intervals. We do not mclude compile time for the (unoptimized) compiler since the paper's focus is the design and optimization of LPSAT; however, compile time can be substantial (e.g., twenty minutes on log-c).

We report on a sequence of problems in the metric logistics domain, which includes all the features of t~e ATT logistics domain [Kautz and Selman, 1996]: air­ planes and trucks moving packages among cities and sites within cities. However, our metric version adds fuel and distances between cities; airplanes and trucks both have individual maximum fuel capacities, consume fuel to move (the amount is per trip for trucks and based on distance between cities for airplanes), and can refuel at depots. log-a through log-d are the same as the ATT problems except for the addition of fuel. easy-1 through easy-4 are simplifications of log-a with more elements re­ tained in the higher numbered problems. We report on highly successful experiment~ with l_earnin~ a_nd _back­ jumping as well as two other mterestmg optimizatiOns.

6.1 Learning and Backjumping

The results in Figure 7 demonstrate the improvement in solving times resulting from activating t_he l~arning and backjumping facilities which were descnbed m Sec­ tion 4. Runs were cut off after one hour of solve time (the minimal conflict set technique ran over an hour only on log-d). Without learning or backjumping LPSAT quickly exceeds the maximum time allotted to it. With learning and backjumping activated using global conflict sets, the solver handles larger problems and runs faster . Our best method, minimal conflict sets, quickly solves even some of the harder problems in the metric logistics domain.

6.2 Splitting Heuristic

Line 7 of the LPSAT pseudocode (Figure 3) makes a non­ deterministic choice of variable v before the recursive call, and the splitting heuristic used to guide this choice can bias performance. We expected the standard RELSAT heuristic to perform poorly (due to a overly strong pref­ erence for trigger variables) for two reasons: 1) the trig­ ger itself is an implicit clause whic~ is resolved when _a trigger variable is set, and 2) each time the solver modi­ fies a trigger variable, it may call CASSOWARY, and these calls often dominate runtime. We tried several methods of including information about the trigger variables in the splitting heuristic, including adding and multiplying the score of trigger variables by a user-settable prefer­ ence value. To our surprise, however, we were unable to achieve significant improvement (although incre~sing the preference for trigger variables did slow executiOn). These results lead us to suspect that either that LCNF problems are generally insensitive to our heuristics or that our compilation of metric planning domains already encodes information about trigger variables in the struc­ ture of the problem. Further experiments will decide the issue.

6.3 Random Restarts

Because LPSAT uses a randomized backtracking algo­ rithm and because early experimental results showed a small percentage of runs far exceeded the me?ian run­ time, we experimented with random restarts usmg a pro­ cess similar to the one described in [Gomes et al., 1998] . We cut off solving at a deadline - which can be ei­ ther fixed beforehand or geometrically increasing - and restart the solver with a new random seed.

Figure 8 shows the results of these experiments. We first ran the algorithm twenty times on each problem to produce the "Raw" entries 4 . Then, we calculated the cutoff time which minimized the expected runtime of the system based on these twenty runs. Finally, we reran the problems with this tuned cutoff time to produce the "Tuned Cutoff" data.

4 All three sets of runs use minimal conflict sets, learning, and backjumping.

While this technique provides some speedup on log-b and impressive speedup on log-e, it requires substantial, preliminary research into the difficulty of the problem (in order to determine the appropriate cutoff time). Unless LPSAT is being used repeatedly to solve a single problem or several very similar problems, the process of finding good restart times will domi.nate overall runtime.

Therefore, we also experimented with a restart system which requires no prior analysis. This "Cutoff doubling" approach sets an initial restart limit of one second and increases that limit by a factor of two on each restart until reaching a solution. We have not yet performed any theoretical analysis of the effectiveness of this technique, but Figure 8 demonstrates a small improvement. More interesting than the average improvement, however, is the fact that this method improved the consistency of the runtimes on the harder problems; indeed, on log-e five of the twenty "Raw" runs lasted longer than the longest "Cutoff doubling" run.

7 Related Work

Limited space precludes a survey of propositional satis­ fiability algorithms and linear programming methods in this paper. See [Cook and Mitchell, 1997] for a survey of satisfiability and [Karloff, 1991] for a survey of linear programming.

Our work was inspired by the idea of compiling prob­ abilistic planning problems to MAJSAT [Majercik and Littman, 1998]. It seemed that if one could extend the SAT "virtual machine" to support probabilistic reason­ ing, then it would be useful to consider the orthogonal extension to handle metric constraints.

Other researchers have combined logical and con­ straint reasoning, usually in the context of programming languages. CLPR may be thought of as an integration of Prolog and linear programming, and this work intro­ duced the notion of incremental Simplex [Jaffar et al., 1992] . Saraswat's thesis [Saraswat, 1989] formulates a family of programming languages which operate through the incremental construction of a constraint framework. CHIP [Van Hentenryck, 1989] augments logic program­ ming with the tools to efficiently solve constraint satis­ faction problems (e.g., consistency checking), but deals only with variables over finite domains. NUMERICA ex­ tends this work by adding a variety of differential equa­ tion solvers to the mix [Van Hentenryck, 1997]. Hooker et a!. describe a technique for combining linear program­ ming and constraint propagation [Hooker et al., 1999].

BLACKBOX uses a translate/solve/decode scheme for planning and satisfiability [Kautz and Selman, 1998]. ZENO is a causal link temporal planner which handled resources by calling an incremental Simplex algorithm within the plan-refinement loop [Penberthy and Weld, 1994]. The GRAPHPLAN [Blum and Furst, 1995] descen­ dant IPP has also been extended to handle metric rea­ soning in its plan graph [Koehler, 1998]. SIPE [Wilkins,

1990] and OPLAN [Currie and Tate, 1991] are indus­ trial strength planners which include resource planning capabilities. Two recent systems address the metric planning problem using compilation to integer program­ ming [Kautz and Walser, 1999; Vossen et al., 1999J.

8 Conclusions and Future Work

LPSAT is a promising new technique that combines the strengths of fast satisfiability methods with an incremen­ tal Simplex algorithm to efficiently handle problems in­ volving both propositional and metric reasoning. This paper makes the following contributions:

• We defined the LCNF formalism for combining boolean satisfiability with linear (in)equalities.
• We implemented the LPSAT solver for LCNF by com­ bining the RELSAT satisfiability solver [Bayardo and Schra&, 1997] with the CASSOWARY constraint rea­ soner [Badros and Borning, 1998].
• We experimented with three optimizations for LPSAT: adapting the splitting heuristic to trigger variables, adding random restarts, and incorporat­ ing learning and backjumping. Using minimal con­ flict sets to guide learning and backjumping pro­ vided four orders of magnitude speedup.
• We implemented a compiler for resource planning problems. LPSAT's performance with this compiler was much better than that of ZENO [Penberthy and Weld, 1994].

Much remains to be done. There are many ways we could improve the compiler: improving its runtime by optimizing exclusion detection, exploring new exclusion encodings, optimizing the number of constraints used for influences, and improving our handling of conditional ef­ fects. In addition, we wish to investigate the issue of tun­ ing restarts to problems, including a thorough investiga­ tion of exponentially growing resource limits. It would also be interesting to implement an LCNF solver based on a stochastic engine. We hope to add support for more expressive constraints by adding nonlinear solvers.