SAS+ planning as satisfiability (Q2887072)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: SAS+ planning as satisfiability |
scientific article; zbMATH DE number 6035677
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | SAS+ planning as satisfiability |
scientific article; zbMATH DE number 6035677 |
Statements
16 May 2012
0 references
search
0 references
planning as satisfiability
0 references
SAT solvers
0 references
SAS+ encoding of actions and planning problems
0 references
SAS+ planning as satisfiability (English)
0 references
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.
0 references
