A novel transition based encoding scheme for planning as satisfiability

Ruoyun Huang, Yixin Chen, Weixiong Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

40 Scopus citations

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 STRlPS-based encoding, in terms of both time and memory efficiency.

Original languageEnglish
Title of host publicationAAAI-10 / IAAI-10 - Proceedings of the 24th AAAI Conference on Artificial Intelligence and the 22nd Innovative Applications of Artificial Intelligence Conference
PublisherAI Access Foundation
Pages89-94
Number of pages6
ISBN (Print)9781577354642
StatePublished - 2010
Event24th AAAI Conference on Artificial Intelligence and the 22nd Innovative Applications of Artificial Intelligence Conference, AAAI-10 / IAAI-10 - Atlanta, GA, United States
Duration: Jul 11 2010Jul 15 2010

Publication series

NameProceedings of the National Conference on Artificial Intelligence
Volume1

Conference

Conference24th AAAI Conference on Artificial Intelligence and the 22nd Innovative Applications of Artificial Intelligence Conference, AAAI-10 / IAAI-10
Country/TerritoryUnited States
CityAtlanta, GA
Period07/11/1007/15/10

Fingerprint

Dive into the research topics of 'A novel transition based encoding scheme for planning as satisfiability'. Together they form a unique fingerprint.

Cite this