A Novel Transition Based Encoding Scheme for Planning as Satisfiability
Yixin Chen
Associate Professor
Computer Science and Engineering
Washington University in St Louis
Abstract :
Planning as satisfiability is a principal approach to planning with many eminent advantages. The existing plan- ning as satisfiability
techniques usually use encodings compiled from the STRIPS formalism. We introduce a novel SAT encoding scheme based on the SAS+ formal- ism. 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.
Bio:
Yixin Chen is an Associate Professor of Computer Science at the Washington University in St Louis. His research interests include planning
and scheduling, combinatorial optimization, and data mining. He received his Ph.D. from University of Illinois at Urbana-Champaign in 2005. His work on planning has won First Prizes in the International Planning Competitions (2004 & 2006) and the Best Paper Award at the AAAI-10 and ICTAI-05 conferences. He has received an Early Career Principal Investigator Award from the Department of Energy (2006) and a Microsoft Research New Faculty Fellowship (2007). He serves on the Editorial Board of Journal of Artificial Intelligence Research (JAIR) and IEEE Transactions on Knowledge and Data Engineering (TKDE), and as a Guest Editor for ACM Transactions on Intelligent Systems and Technology.