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

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)

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.

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

(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
• scientific article; zbMATH DE number 1954197 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 1560491 (Why is no real title available?)

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)