💻 computer science

An ASP-based approach to Solving General Stochastic Two-Player Games

本文介绍了随机答案集编程（SQASP），这是首个基于答案集编程（ASP）的方法，用于求解具有不确定性的双人轮流制通用游戏描述语言（GDL）游戏，并展示了其在小型随机博弈中与正向搜索的竞争力以及在终局评估方面的潜力。

原作者： Yifan He, Michael Thielscher

发布于 2026-05-25

📖 1 分钟阅读☕ 轻松阅读

原作者： Yifan He, Michael Thielscher

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在教一台电脑如何玩棋盘游戏。通常，这类游戏就像国际象棋：你走一步，对手走一步，棋盘以一种可预测的方式发生变化。但如果游戏还涉及一张“万能牌”呢？如果你走了一步后，一次魔法般的骰子投掷决定了你的走法是否有效，或者一位看不见的第三方（我们称他为“随机”）往齿轮里扔了一把扳手，会怎样？

本文旨在教导计算机解决这些棘手且不可预测的游戏。作者 Yifan He 和 Michael Thielscher 构建了一套新的数学工具包，用于在涉及运气的情况下找出最佳策略。

以下是他们方法的分解，使用了简单的类比：

1. 问题：“随机”玩家

在标准博弈论中，计算机擅长计算针对聪明对手的完美走法。但当你加入随机性（如掷骰子或抽牌）时，数学就会变得混乱。

旧方法：以前的计算机程序可以处理两个聪明玩家的游戏（如国际象棋），或者一个玩家加随机元素的游戏（如单人纸牌）。但它们无法同时处理两个聪明玩家加一个随机元素的游戏。
目标：作者希望解决“通用随机双人博弈”。这就像玩井字棋，但每次你试图放置一个 X 时，都有 30% 的概率该格子会变成 O，或者有 50% 的概率该走法被完全阻挡。

2. 新工具：SQASP（“魔法蓝图”）

作者发明了一种名为**随机答案集编程（SQASP）**的新语言。

类比：想象你是一位建筑师，正在设计一座房子。你有一张蓝图（游戏规则）。过去，你只能为两种特定类型的建造者设计房屋：一位是天才战略家（对手），另一位是严格遵守规则的机器人。
创新：SQASP 就像一种新型蓝图，可以描述一个施工现场，那里有一位天才战略家、一位机器人和一位赌徒共同工作。
- 天才（玩家 X）想要获胜。
- 对手（玩家 O）想要阻止玩家 X。
- 赌徒（随机）抛硬币来决定接下来发生什么。
SQASP 允许计算机提问：“假设我的对手完美地阻止我，而赌徒随心所欲，我获胜的最高可能概率是多少？”

3. 翻译器：将蓝图转化为谜题

计算机不懂“蓝图”。它们懂“逻辑谜题”。

过程：作者构建了一个翻译器（名为 sqasp2xssat 的工具）。它将 SQASP 蓝图转换为一个巨大的逻辑谜题，称为扩展随机可满足性（XSSAT）。
隐喻：把 SQASP 想象成一份复杂的蛋糕食谱。翻译器是一台机器，将这份食谱转化为一个巨大的、多层级的数独谜题。一旦解开谜题，答案就会告诉你获胜的确切概率。
求解器：他们使用现有的求解器（SharpSSAT）来破解这个数独。如果求解器说“是的，这个谜题可以解决”，那就意味着玩家拥有获胜策略。如果它计算出 67% 的概率，那就是最佳可能结果。

4. “量词移位”技巧

本文还测试了一种特定的优化技术，称为量词移位。

类比：想象你在组织一场比赛。
- 方法 A（基线）：你列出每个玩家的每一步走法，然后检查走法是否合法，最后检查游戏是否结束。
- 方法 B（移位）：你在列出走法之前就先检查走法是否合法。这似乎更快，因为你不会浪费时间去规划那些非法的走法。
结果：在只有两个聪明玩家的游戏（确定性游戏）中，这种“移位”技巧带来了巨大的速度提升。然而，作者发现，在包含“赌徒”的游戏（随机游戏）中，这种技巧并没有带来太大差异。
原因：他们使用的求解器（SharpSSAT）非常聪明。它内置了一个“侦探”（称为单元传播），无论指令给出的顺序如何，它都能自行找出非法走法。因此，对于这种特定的求解器来说，这种复杂的重新排序是不必要的。

5. 结果：表现如何？

团队在经典游戏的变体上测试了他们的系统，如井字棋、四子棋和尼姆游戏，但加入了“随机”玩家。

性能：他们的新方法与标准的“前向搜索”方法（即计算机在脑海中模拟数百万次游戏以观察结果）具有竞争力。
局限：该方法在小棋盘（如 3x3 或 4x4）上表现良好。然而，当游戏变得太大时（例如尼姆游戏中有 100 个棋子的堆），逻辑谜题会变得过于庞大，计算机无法在合理的时间内解决。
启示：该方法非常适合终局评估。如果游戏接近尾声，该系统可以告诉通用游戏 AI：“嘿，如果你走这一步，你有 99% 的获胜概率”，从而帮助其做出最终决策。

总结

作者创造了一种新的数学方法来描述运气与策略碰撞的游戏。他们将这些描述转化为计算机可以求解的逻辑谜题，以找出获胜的“最佳可能概率”。虽然它并非适用于所有游戏规模的灵丹妙药，但它证明了我们可以利用逻辑编程来解决复杂且不确定的游戏，让计算机在混乱的世界中拥有更好的思考未来的方式。

他们未声称的内容：

他们并未声称该方法适用于你看不到整个棋盘的游戏（如扑克或战争井字棋）。他们明确指出，该方法适用于所有人都能看到整个棋盘的游戏（完全信息博弈）。
他们并未声称这将立即取代所有其他 AI 方法；他们指出，这是一种针对特定场景（特别是终局）的替代方案。

技术摘要：基于 ASP 求解通用随机双人博弈的方法

问题陈述

通用博弈（GGP）系统旨在根据运行时描述进行策略博弈，而无需预先了解规则。博弈描述语言（GDL）及其扩展 GDL-II 是规范此类博弈的标准形式化方法，其中 GDL-II 支持随机性（随机性）和部分可观测性。虽然答案集编程（ASP）已成功应用于求解确定性的单人和双人 GDL 博弈，但现有的 ASP 框架缺乏同时表达对抗性（极小化极大）和随机性行为的能力。因此，在使用基于 ASP 的方法求解涉及不确定性的双人轮流 GDL 博弈方面存在空白。

方法论

作者提出了一种通过引入新语言和基于翻译的求解器来解决双人随机 GDL 博弈的新方法。

1. 随机量化答案集编程（SQASP）

为了弥合 ASP 与随机博弈求解之间的差距，本文引入了SQASP，这是一种在量化 ASP（QASP）基础上扩展了概率量词的语言。

语法：SQASP 程序的形式为 $Q_1.x_1 \dots Q_n.x_n \ P$ ，其中 $P$ 是一个普通逻辑程序，量词 $Q_i$ 可以是存在量词（ $\exists$ ）、全称量词（ $\forall$ ）或概率量词（ $\mathcal{R}_{p}$ ）。
语义：满足 SQASP 程序的最大概率被递归定义。概率量词 $\mathcal{R}_{p}$ 为变量为真分配概率 $p$ ，并根据子公式的概率计算期望值。
翻译：作者实现了一个工具 sqasp2xssat，将 SQASP 程序翻译为**扩展随机可满足性（XSSAT）**公式。XSSAT 在量化布尔公式（QBF）的基础上扩展了概率量词。该翻译利用现有工具（如 lp2sat）将逻辑程序 $P$ 转换为合取范式（CNF）公式 $\psi$ ，其模型对应于 $P$ 的稳定模型。

2. 将 GDL 博弈编码为 SQASP

核心贡献是构建一个 SQASP 程序 $\Psi$ ，使其最大可满足概率等于玩家 $x$ 在 $n$ 步内的最大获胜概率（ $P_x^w(S_0, n)$ ）。编码分为两个主要阶段：

合作基线：首先，构建一个逻辑程序 $P_c$ ，假设所有玩家（包括对手 $o$ 和随机玩家 $r$ ）都合作以达到 $x$ 获胜的终止状态。这确保了有效的博弈进程、在 $n$ 步内终止以及目标状态的达成。
对抗与随机建模：随后扩展程序以捕捉对手和环境的具体行为：
- 对抗性玩家（ $o$ ）：使用决策变量（dec_o）上的全称量化（ $\forall$ ）进行建模。这迫使求解器考虑对手最小化 $x$ 获胜概率的最坏情况。编码采用动作的对数表示以减少规则数量。
- 随机玩家（ $r$ ）：使用概率量词（ $\mathcal{R}_{1/i}$ ）进行建模。编码确保如果博弈尚未终止，随机玩家将从可用的合法移动中均匀地选择恰好一个合法动作。这是通过计算合法动作数量并将概率约束应用于决策变量（dec_r）来实现的。

3. 量化策略

本文研究了所得 XSSAT 公式的两种量化策略：

基线方法（ $Q_b$ ）：所有非选择原子（例如 legal、terminal）被放置在最内层的存在量词块中，遵循选择原子的严格时间顺序。
基于依赖的方法（ $Q_d$ ）：受确定性博弈技术的启发，该方法将非选择原子尽可能早地移至量词前缀中，紧跟在其所依赖的选择原子之后。这旨在通过在对 does 进行分支之前固定 legal 等值来减少搜索空间。

主要贡献

首个基于 ASP 的随机 GDL 求解器：本文提出了首个使用 ASP 求解双人、随机、轮流 GDL 博弈的方法。
SQASP 语言：引入了随机量化答案集编程，在逻辑编程框架内统一了对抗性和随机性推理。
基于翻译的求解器：开发了 sqasp2xssat，将 SQASP 程序转换为 XSSAT 公式，从而能够使用现有的 XSSAT 求解器（特别是 SharpSSAT）进行博弈求解。
理论正确性：作者提供了形式化证明（定理 2 和定理 3），确立了 GDL 博弈中的最大获胜概率与生成的 SQASP/XSSAT 公式的最大可满足概率之间的等价性。

实验结果

作者在井字棋、四子棋和尼姆博弈的随机变体上评估了他们的方法，将基于 SQASP 的方法（使用 $Q_b$ 和 $Q_d$ 两种量化）与前向搜索期望极小化极大（EMM）求解器进行了比较。

性能：基于 ASP 的方法在小型随机博弈上与前向搜索具有竞争力。在许多实例中（例如井字棋、三子棋），ASP 求解器计算的获胜概率与 EMM 相当，且通常耗时相似。
量词移位：令人惊讶的是，在使用 SharpSSAT 求解器时，基于依赖的量化（ $Q_d$ ）并未比基线（ $Q_b$ ）带来显著的性能提升。作者将此归因于 SharpSSAT 内部的单元传播机制，该机制无论量词顺序如何都能推导出原子（如 legal）的值，从而有效地缓解了对显式移位的需求。
可扩展性限制：该方法在处理较大的状态空间时面临困难，例如具有大堆大小的随机尼姆博弈。生成的 XSSAT 公式变得过大（超过一百万个子句），现有求解器难以高效处理，而 EMM 由于动态规划和转置表而具有良好的可扩展性。

意义与主张

本文声称，所提出的基于 ASP 的方法为通用博弈系统中的终局评估提供了一种可行的替代方案。通过将 ASP 在确定性博弈中的成功应用扩展到随机领域，这项工作证明了逻辑编程可以有效地处理不确定性和对抗性推理。

作者谦逊地指出，虽然该方法并未在所有情况下都优于前向搜索（特别是对于具有非常大状态空间或特定结构如尼姆博弈的博弈），但它成功地将先前针对确定性博弈的结果推广到了随机博弈。他们确定将扩展至部分可观测性（例如扑克、战争井字棋）是未来工作的关键方向，并承认当前方法仅限于完全信息博弈。