Paper Info
Title
Combining linear programming and satisfiability solving for resource planning
Abstract
Compilation to Boolean satisfiability has become a powerful paradigm for solving artificial intelligence problems. However, domains that require metric reasoning cannot be compiled efficiently to satisfiability even if they would otherwise benefit from compilation. We address this problem by combining techniques from the artificial intelligence and operations research communities. In particular, we introduce the LCNF (Linear Conjunctive Normal Form) representation that combines propositional logic with metric constraints. We present LPSAT (Linear Programming plus SATisfiability), an engine that solves LCNF problems by interleaving calls to an incremental Simplex algorithm with systematic satisfaction methods. We explore several techniques for enhancing LPSAT's efficiency and expressive power by adjusting the interaction between the satisfiability and linear programming components of LPSAT. Next, we describe a compiler that converts metric resource planning problems into LCNF for processing by LPSAT. Finally, the experimental section of the paper explores several optimisations to LPSAT, including learning from constraint failure and randomised cutoffs.
Year
DOI
Venue
2001
10.1017/S0269888901000017
Knowledge Eng. Review
Keywords
Field
DocType
artificial intelligence,linear programming,metric resource planning problem,boolean satisfiability,constraint failure,linear conjunctive normal form,lcnf problem,metric reasoning,artificial intelligence problem,metric constraint,linear program,satisfiability
Simplex algorithm,Computer science,Satisfiability,Boolean satisfiability problem,Propositional calculus,Compiler,Theoretical computer science,Conjunctive normal form,Linear programming,Interleaving
Journal
Volume
Issue
ISSN
16
1
0269-8889
Citations 
PageRank 
References 
25
1.55
22
Authors
2
Name
Order
Citations
PageRank
Steven A. Wolfman144959.00
Daniel S. Weld2102981127.49