Introduction

Recent advances in satisfiability (SAT) solving technology have rendered large, previously intractable problems quickly solvable [Crawford and Auton1993,Selman et al.1996,Cook and Mitchell1997,Bayardo and Schrag1997,Li and Anbulagan1997,Gomes et al.1998]. SAT solving has become so successful that many other difficult tasks are being compiled into propositional form to be solved as SAT problems. For example, SAT-encoded solutions to graph coloring, planning, and circuit verification are among the fastest approaches to these problems [Kautz and Selman1996,Selman et al.1997].

But many real-world tasks have a metric aspect. For instance, resource planning, temporal planning, scheduling, and analog circuit verification problems all require reasoning about real-valued quantities. Unfortunately, metric constraints are difficult to express in SAT encodings³. Hence, a solver which could efficiently handle both metric constraints and propositional formulae would yield a powerful substrate for handling AI problems.

This paper introduces a new problem formulation, LCNF, which combines the expressive power of propositional 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 explores 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: learning 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 backjumping; LPSAT learns new clauses by discovering explanations 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 crucial in order to learn effectively from constraint conflicts.

Figure 1: Data flow in the demonstration resource planning system; space precludes discussion of the grey components.

1.0figs/sys6.eps

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 [McDermott1998] based on the metric constructs used by metric IPP [Koehler1998]), including a metric version of the ATT Logistics domain [Kautz and Selman1996].