Automatic SAT-Compilation of Planning Problems
Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence. Planning and Scheduling. Pages 1169-1176.
Abstract
Recent work by Kautz et al. provides tantalizing evidence that large, classical planning problems may be efficiently solved by translating them into propositional satisfiability problems, using stochastic search techniques , and translating the resulting truth assignments back into plans for the original problems. We explore the space of such transformations , providing a simple framework that generates eight major encodings (generated by selecting one of four action representations and one of two frame axioms) and a number of subsidiary ones. We describe a fully-implemented compiler that can generate each of these encodings, and we test the compiler on a suite of STRIPS planning problems in order to determine which encodings have the best properties.
@inproceedings{ijcai1997p169,
title = {Automatic SAT-Compilation of Planning Problems},
author = {Ernst, Michael D. and Millstein, Todd D. and Weld, Daniel S.},
booktitle = {Proceedings of the Fifteenth International Joint Conference on
Artificial Intelligence, {IJCAI-97}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Martha E. Pollack},
pages = {1169--1176},
year = {1997},
note = {Planning and Scheduling},
url = {https://ijcai.org/proceedings/1997/169},
}
TY - CPAPER TI - Automatic SAT-Compilation of Planning Problems AU - Ernst, Michael D. AU - Millstein, Todd D. AU - Weld, Daniel S. T2 - Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, IJCAI-97 PB - International Joint Conferences on Artificial Intelligence PY - 1997 SP - 1169 EP - 1176 UR - https://ijcai.org/proceedings/1997/169 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
