Thematic image University of Washington Computer Science & Engineering
 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

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.


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