The LPSAT Engine & Its Application to Resource Planning
Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence. Challenge Papers. Pages 310-316.
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.
@inproceedings{ijcai1999p46,
title = {The LPSAT Engine & Its Application to Resource Planning},
author = {Wolfman, Steven A. and Weld, Daniel S.},
booktitle = {Proceedings of the Sixteenth International Joint Conference on
Artificial Intelligence, {IJCAI-99}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Thomas Dean},
pages = {310--316},
year = {1999},
note = {Challenge Papers},
url = {https://ijcai.org/proceedings/1999/46},
}
TY - CPAPER TI - The LPSAT Engine & Its Application to Resource Planning AU - Wolfman, Steven A. AU - Weld, Daniel S. T2 - Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, IJCAI-99 PB - International Joint Conferences on Artificial Intelligence PY - 1999 SP - 310 EP - 316 UR - https://ijcai.org/proceedings/1999/46 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
