A Novel Transition Based Encoding Scheme for Planning as Satisfiability
DOI:
https://doi.org/10.1609/aaai.v24i1.7544Keywords:
Planning, Satisfiability, EncodingAbstract
Planning as satisfiability is a principal approach to planning with many eminent advantages. The existing planning as satisfiability techniques usually use encodings compiled from the STRIPS formalism. We introduce a novel SAT encoding scheme based on the SAS+ formalism. It exploits the structural information in the SAS+ formalism, resulting in more compact SAT instances and reducing the number of clauses by up to 50 fold. Our results show that this encoding scheme improves upon the STRIPS-based encoding, in terms of both time and memory efficiency.
Downloads
Published
2010-07-03
How to Cite
Huang, R., Chen, Y., & Zhang, W. (2010). A Novel Transition Based Encoding Scheme for Planning as Satisfiability. Proceedings of the AAAI Conference on Artificial Intelligence, 24(1), 89-94. https://doi.org/10.1609/aaai.v24i1.7544
Issue
Section
Constraints, Satisfiability, and Search