Conclusions and Future Work

LPSAT is a promising new technique that combines the strengths of fast satisfiability methods with an incremental Simplex algorithm to efficiently handle problems involving 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 combining the RELSAT satisfiability solver [Bayardo and Schrag1997] with the CASSOWARY constraint reasoner [Badros and Borning1998].

• We experimented with three optimizations for LPSAT: adapting the splitting heuristic to trigger variables, adding random restarts, and incorporating learning and backjumping. Using minimal conflict sets to guide learning and backjumping provided 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 Weld1994].

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 effects. In addition, we wish to investigate the issue of tuning restarts to problems, including a thorough investigation 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.

=2em =2em