Combining linear programming and satisfiability solving for resource planning

Compilation to Boolean satisfiability has become a powerful paradigm for so lving artificial intelligence problems. However, domains that require metri c reasoning cannot be compiled efficiently to satisfiability even if they w ould otherwise benefit from compilation. We address this problem by combini ng techniques from the artificial intelligence and operations research comm unities. in particular, we introduce the LCNF (Linear Conjunctive Normal Fo rm) representation that combines propositional logic with metric constraint s. We present LPSAT (Linear Programming plus SATisfiability), an engine tha t solves LCNF problems by interleaving calls to an incremental Simplex algo rithm with systematic satisfaction methods. We explore several techniques f or enhancing LPSAT's efficiency and expressive power by adjusting the inter action between the satisfiability and linear programming components of LPSA T. Next, we describe a compiler that converts metric resource planning prob lems into LCNF for processing by LPSAT. Finally, the experimental section o f the paper explores several optimisations to LPSAT, including learning fro m constraint failure and randomised cutoffs.