将FTS转换并编码为SAT求解：什么有帮助，什么有害（扩展版本）

arXiv cs.AI 论文
sat-solving factored-tasks planning encoding ai-planning propositional-logic task-transformations

摘要

本文研究了如何将因子化规划任务（FTS）编码为SAT，提出了多种编码策略，并分析了任务转换对基于SAT的规划性能的影响。其目的是将SAT求解扩展到比启发式搜索更紧凑的规划表示。

arXiv:2605.30563v1 公告类型：新 摘要：因子化任务是一种经典的规划表示，它扩展了SAS+，包含有限形式的析取前提、条件效应和天使非确定性。这使得任务表示比传统的表示法（如STRIPS或SAS+）更加紧凑，并支持多种任务转换。然而，现有的针对因子化任务的规划方法仅限于启发式搜索方法。 在这项工作中，我们研究了如何将因子化任务编码为SAT。我们提出了几种编码任务的方法，重点在于将因子化转换关系转化为命题逻辑的不同策略。我们还分析了在此背景下如何在各个层面利用并行性，并研究了常见任务转换对基于SAT的规划器性能的影响。
查看原文
查看缓存全文

缓存时间: 2026/06/01 09:23 

# 转换和编码FTS以用于SAT求解：哪些有帮助，哪些有损害（扩展版）
Source: https://arxiv.org/abs/2605.30563
View PDF (https://arxiv.org/pdf/2605.30563)

> 摘要：分解任务是一种经典的规划表示，它在SAS+的基础上扩展了有限形式的析取前提、条件效应和天使非确定性。这使得任务的表示比传统形式化（如STRIPS或SAS+）更加紧凑，并支持广泛的任务转换。然而，现有的分解任务规划方法仅限于启发式搜索方法。在这项工作中，我们研究了如何将分解任务编码为SAT问题。我们提出了几种编码任务的方法，重点是将分解的转移关系转换为命题逻辑的不同策略。我们还分析了在此设置中如何在不同层次上利用并行性，并研究了常见任务转换对基于SAT的规划器性能的影响。

## 提交历史

来自：Gregor Behnke [查看电子邮件](https://arxiv.org/show-email/cec7f8d2/2605.30563) **\[v1\]** 2026年5月28日星期四 20:50:52 UTC (662 KB)

相似文章

面向数值全序HTN规划的SMT-based HTN-SAT编码

arXiv cs.AI

本文研究了数值全序HTN（TOHTN）规划，通过使用SMT扩展基于SAT的编码来处理数值流，引入了一个基准测试集，并展示了其作为未来工作基准的竞争性能。

Function-Space Transformer：具有自适应锚点的模型

arXiv cs.LG

本文提出 Function-Space Transformer（FST），一种在连续域上从函数中学习的框架。该框架将特征存储在由输入预测的锚点位置上，并通过递归的函数空间细化进行更新。FST 在 PDEBench 预测任务上优于 Perceiver IO，与 Fourier Neural Operators 表现相当，并在 ImageNet-1K 上以更少的参数超越 ViT。