Oct, 2023

制作一个优秀的雪人是困难的

PDF
TL;DR通过使用 SAT 方法解决难题视频游戏，我们证明了直接将游戏转换为 SAT 显著超过了现有的先进规划器的性能，主要原因是 SAT 能够轻松建模可达性属性，从而获得更短的解决方案。
puzzle video gameoptimality of solutionsplanning problemsatreachability properties
发现论文，激发创造
  • 网格图可达性和益智游戏

    我们研究了求解迷宫类问题的 CP 和 SAT 方法，提出了一种新的可达性编码，并通过实验证明这种新编码在以 SAT 为范式的规划问题中，尤其是考虑到同时执行多个动作时是非常适用的。

    Oct, 2023

  • 迈向《拼图游戏》模型

    我们报告了建模和解决 Puzznic 的进展情况，这是一款需要玩家计划移动序列以匹配方块从而清理网格的视频游戏，我们在没有移动方块的关卡上比较了计划方法和三种约束编程方法在一小组基准实例上的表现，目前计划方法优于约束编程方法，但我们提出了改进约束模型的建议。

    Oct, 2023

  • 建模和解决 PDDL 绘图的挑战

    通过使用 PDDL 对模型 Plotting 进行建模，并采用基于基础的现代化规划器来解决，我们研究了一种基于 Plotting 的规划问题。

    Oct, 2023

  • 基于启发式搜索的物理问题求解方法：PDDL + 中的愤怒的小鸟

    本文研究了如何使用领域无关的规划器和组合搜索来玩《愤怒的小鸟》，使用了 PDDL + 进行了建模，并提出了多个领域特定的增强措施，包括启发式和类似首选操作员的搜索技术，研究对比表明我们的方法在大多数水平上与定制的特定领域解算器的表现相当，即使不使用领域特定的搜索增强措施。

    Mar, 2023

  • 规划复杂转换的初步案例研究：绘图

    介绍了一种约束模型，用于解决将网格减少到给定目标数量或更少的 Plotting 问题，探讨了 AI 规划在建模语言方面的不足，建议富有表达力的建模语言对 AI 规划有益。

    Oct, 2021

  • 用概率方法扩展机器学习以解决组合优化问题的隐蔽博弈

    应用深度学习解决困难的组合问题具有巨大的潜力。该研究侧重于布尔可满足性（SAT）问题，并通过基本的概率方法消除了由于训练集仅限于小于实际问题规模几个数量级的随机公式导致的难题。使用我们的生成器，我们对现有的最先进模型进行训练，以预测具有 10,000 个变量的公式的可满足性，提出了新的分类器，可以对大多数困难水平的相同数据集进行显着改进，从而打破了过去基于公式的句法特征学习的方法，并使用求解器计算的简短前缀进行学习。

    Nov, 2022

  • 利用深度学习构建带性能界限的随机局部搜索 SAT 求解器

    利用图神经网络训练适用于布尔可满足性问题的 SLS 求解器，可显著提高性能，平均解决比例更高、步骤更少，具有性能保证。

    Sep, 2023

  • 通过非确定性约束逻辑模型计算的滑块拼图和其他问题的 PSPACE 完备性

    本文介绍了一种基于加权有向图和最小流限制的非确定性计算模型，并且通过一系列特例的证明和简单归约，证明了该模型可以被用于解决复杂的运动规划问题，包括障碍物移动、滑动积木等。

    May, 2002

  • 一种基于符号 SAT 的 POMDP 几乎必达性小策略算法

    研究 POMDPs 的几乎确定可达性问题，提出了具有小内存的策略的符号算法，通过有效编码到 SAT 并使用 SAT solver 来解决问题。

    Nov, 2015

  • NL2Plan: 从最简文本描述中驱动的鲁棒性 LLM 规划

    NL2Plan 是第一个通用领域脱机驱动计划系统，利用大型语言模型通过逐步提取必要信息从短文本提示创建完整的 PDDL 描述，进而通过经典计划器解决问题，提供解决 15 个任务中 10 个任务的改进以及提高可解释性和 PDDL 创建协助工具的功能。

    May, 2024