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