A Novel Transition Based Encoding Scheme for Planning as Satisfiability
Abstract
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.
Cite
Text
Huang et al. "A Novel Transition Based Encoding Scheme for Planning as Satisfiability." AAAI Conference on Artificial Intelligence, 2010. doi:10.1609/AAAI.V24I1.7544Markdown
[Huang et al. "A Novel Transition Based Encoding Scheme for Planning as Satisfiability." AAAI Conference on Artificial Intelligence, 2010.](https://mlanthology.org/aaai/2010/huang2010aaai-novel/) doi:10.1609/AAAI.V24I1.7544BibTeX
@inproceedings{huang2010aaai-novel,
title = {{A Novel Transition Based Encoding Scheme for Planning as Satisfiability}},
author = {Huang, Ruoyun and Chen, Yixin and Zhang, Weixiong},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2010},
pages = {89-94},
doi = {10.1609/AAAI.V24I1.7544},
url = {https://mlanthology.org/aaai/2010/huang2010aaai-novel/}
}