将可分解任务转化为SAT求解，提升规划效率与灵活性。
Transforming and Encoding FTS for SAT Solving: What Helps, What Hurts (Extended Version)
- 提出多种将可分解任务的转移关系编码为命题逻辑的方法。
- 实验证明特定编码策略能显著降低SAT求解时间。
- 适合对规划系统性能优化的研究者参考。
可分解任务是经典规划表示法，扩展了SAS+，支持有限的析取前提、条件效应和天使式非确定性，相较于STRIPS或SAS+等传统形式化方法，能更紧凑地表示任务，并支持广泛的任务变换。然而，现有的可分解任务规划方法仅限于启发式搜索。本文研究如何将可分解任务编码为SAT问题，提出多种将可分解转移关系转换为命题逻辑的策略，并分析在该设置下多级并行性的利用方式，以及常见任务变换对基于SAT的规划器性能的影响。
原文摘要 · Abstract (English)
Factored tasks are a classical planning representation that extends SAS+ with limited forms of disjunctive preconditions, conditional effects, and angelic nondeterminism. This allows for a more compact representation of tasks than traditional formalisms such as STRIPS or SAS+, and supports a wide range of task transformations. However, existing planning approaches for factored tasks have been limited to heuristic search methods. In this work, we investigate how to encode factored tasks in SAT. We propose several ways to encode the tasks, focusing on different strategies for translating the factored transition relation into propositional logic. We also analyze how to exploit parallelism at various levels in this setting and study the impact of common task transformations on the performance of SAT-based planners.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。