SAS+ planning as satisfiability

DOI10.1613/JAIR.3442zbMATH Open1244.68071arXiv1401.4598OpenAlexW3100276112WikidataQ129489491 ScholiaQ129489491MaRDI QIDQ2887072FDOQ2887072

Authors: R. Huang, Yixin Chen, Weixiong Zhang 

Publication date: 16 May 2012

Published in: The Journal of Artificial Intelligence Research (JAIR) (Search for Journal in Brave)

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 STRIPS. We introduce a novel SAT encoding scheme (SASE) based on the SAS+ formalism. The new scheme exploits the structural information in SAS+, resulting in an encoding that is both more compact and efficient for planning. We prove the correctness of the new encoding by establishing an isomorphism between the solution plans of SASE and that of STRIPS based encodings. We further analyze the transition variables newly introduced in SASE to explain why it accommodates modern SAT solving algorithms and improves performance. We give empirical statistical results to support our analysis. We also develop a number of techniques to further reduce the encoding size of SASE, and conduct experimental studies to show the strength of each individual technique. Finally, we report extensive experimental results to demonstrate significant improvements of SASE over the state-of-the-art STRIPS based encoding schemes in terms of both time and memory efficiency.

Full work available at URL: https://arxiv.org/abs/1401.4598

Recommendations

• Encoding domain and control knowledge for propositional planning
• Friends or foes? On planning as satisfiability and abstract CNF encodings
• Logics in Artificial Intelligence
• Planning as constraint satisfaction: Solving the planning graph by compiling it into CSP
• Planning as satisfiability: heuristics

zbMATH Keywords

searchSAT solversplanning as satisfiabilitySAS+ encoding of actions and planning problems

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Searching and sorting (68P10)

Cited In (18)

• Planning for hybrid systems via satisfiability modulo theories
• plasp 3: towards effective ASP planning
• Lilotane: a lifted SAT-based approach to hierarchical planning
• Planning as satisfiability: parallel plans and algorithms for plan search
• Title not available (Why is that?)
• Logics in Artificial Intelligence
• Friends or foes? On planning as satisfiability and abstract CNF encodings
• Modification strategies for SAT-based plan adaptation
• Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning
• Planning as quantified Boolean formula
• Encoding domain and control knowledge for propositional planning
• Planning as satisfiability with IPC simple preferences and action costs
• Using satisfiability for non-optimal temporal planning
• Introducing preferences in planning as satisfiability
• plasp 3: towards effective ASP planning
• Compact and efficient encodings for planning in factored state and action spaces with learned binarized neural network transition models
• Planning as satisfiability: heuristics
• Title not available (Why is that?)

Uses Software

• Chaff

This page was built for publication: SAS+ planning as satisfiability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2887072)