SAS+ planning as satisfiability

DOI10.1613/JAIR.3442MaRDI QIDQ2887072zbMATH OpenOpenAlexWikidataFDO

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)

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

zbMATH Keywords

planning as satisfiabilitySAS+ encoding of actions and planning problemsSAT solverssearch

Mathematics Subject Classification ID

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

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.

Review text

The article describes a new encoding for planning as satisfiability called SASE. The encoding is based on the so-called SAS+ formalism and encodes transitions into a satisfiability scheme for SAT solvers replacing the common STRIPS-based encodings of actions. The resulting encoding is more compact than previous encodings yielding significant performance and memory gains. The authors provide a detailed explanation of the benefits of their encoding and present further reduction techniques. A comprehensive empirical study using AI planning benchmarks and a review of related work complement the theoretical results.

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

Cited in

(19)

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

Describes a project that uses

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)