The LPSAT Engine & its Application to Resource Planning¹²

Steven A. Wolfman Daniel S. Weld
Department of Computer Science & Engineering
University of Washington, Box 352350
Seattle, WA 98195-2350 USA
{wolf, weld}@cs.washington.edu

Abstract:

Compilation to boolean satisfiability has become a powerful paradigm for solving AI problems. However, domains that require metric reasoning cannot be compiled efficiently to SAT even if they would otherwise benefit from compilation. We address this problem by introducing the LCNF representation which combines propositional logic with metric constraints. We present LPSAT, an engine which solves LCNF problems by interleaving calls to an incremental simplex algorithm with systematic satisfaction methods. We describe a compiler which converts metric resource planning problems into LCNF for processing by LPSAT. The experimental section of the paper explores several optimizations to LPSAT, including learning from constraint failure and randomized cutoffs.