将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)

相似文章

Transformer线性表示高度结构化的世界模型

arXiv cs.LG

本文证明，在数独求解轨迹上训练的Transformer构建了由领域约束组织的结构化世界模型，并识别出一个稀疏、单语义的电路，负责裸单决策规则。该工作为Transformer在组合任务上的推理提供了完全可解释的算法描述。

FocuSFT：面向稀释感知长上下文微调的双层优化

Hugging Face Daily Papers

本文介绍了 FocuSFT，这是一种双层优化框架，它通过参数化记忆机制解决注意力稀释问题，从而提升长上下文语言模型的性能。在 BABILong 和 RULER 等基准测试中，该框架在准确性和上下文参与度方面均展现出显著提升。

FrontierSmith: 大规模合成开放式编程问题

Hugging Face Daily Papers

FrontierSmith 自动从封闭式任务中生成多样化的开放式编程问题，通过增强的智能体交互和训练数据合成，提升 LLM 在基准测试中的编码性能。