LPSAT

CSE Home

AI Home

About Us

Search

Contact Info

Project faculty  Dan Weld Project students  Steve Wolfman

LPSAT Two Great Systems that Go Great Together The LPSAT project investigates the benefits of combining two powerful reasoning systems: Linear Programming (LP) and Boolean Satisfiability (SAT). Linear Programming is used to represent problems dealing with numerical values and constraints. LP problems can be solved quickly, and are amenable to global analysis. Boolean Satisfiability is used to represent logical problems and can represent disjunction (which LP cannot), but SAT is a harder problem in the worst case than LP. LPSAT combines these systems to create a new representation which can efficiently handle logical disjunction as well as numerical constraints. The LPSAT project has produced a solution engine (enigmatically termed: LPSAT), an input language for LPSAT called LCNF, and an application system which uses LPSAT to solve metric planning problems. Ongoing research on the project studies communication of heuristic information between the systems, new application problems which can be encoded into LPSAT (such as temporal planning), and improved expressiveness in LPSAT encodings. Publications Wolfman and Weld. The LPSAT system and its Application to Resource Planning. In Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence. 1999. Wolfman and Weld. The LPSAT system and its Application to Resource Planning TR 99-04-04. (Slightly expanded from the conference publication.) Wolfman and Weld. Combining Linear Programming and Satisfiability Solving for Resource Planning. In The Knowledge Engineering Review, 16(1):85–99, 2001. Source Code Some background will be helpful before diving into the source. LPSAT was built on top of three existing systems. A modified version of the compiler from Koehler's IPP planning system compiles planning problems to LCNF. The solution engine that solves these problems is a hybrid of Badros and Borning's Cassowary linear constraint solver and Bayardo and Schrag's RelSAT satisfiability solver. Intuitively, the LPSAT planner calls IPP to compile to LCNF and then explores the SAT solution space with RelSAT, making side calls to Cassowary's incremental LP solver each time a SAT variable fires an LP constraint. In practice, much of the added logic in LPSAT is targetted at making these constraints fire at appropriate times and, algorithmically or heuristically, optimizing the search in the presence of constraints. Knowing this will help you understand the structure of the LPSAT code, such as it is. That said, you're now ready for the source code. You're free to use this code for any purpose consistent with the licenses of its various components, but please (1) tell us at the UW when you grab it and what you're up to and (2) do not use the code for evil. Please direct questions about the code to Steve Wolfman <wolf@cs.washington.edu>; I'll help as much as I can. Source code as a tarball Some hints to get you started (Note: these are included in the tarball.)

	Computer Science & Engineering University of Washington Box 352350 Seattle, WA  98195-2350 (206) 543-1695 voice, (206) 543-2969 FAX [comments to Steve Wolfman]