💻 computer science

Solving QBF with Counterexample Guided Refinement

本文介绍了两种用于量化布尔公式（QBF）求解的新颖反例引导抽象精炼（CEGAR）方法——一种递归式 CEGAR 驱动算法和一种基于 DPLL 的学习增强方法——两者在特定问题族上的表现均优于现有求解器。

原作者： Mikoláš Janota, William Klieber, Joao Marques-Silva, Edmund Clarke

发布于 2026-08-17

📖 1 分钟阅读☕ 轻松阅读

原作者： Mikoláš Janota, William Klieber, Joao Marques-Silva, Edmund Clarke

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

想象一下，你是一名正在试图解开一个巨大、多层谜团的侦探，而线索就隐藏在一个巨大的、纠缠不清的线团之中。这不仅仅是一个普通的谜题；这是一场在两个隐形对手之间进行的博弈：一个想要证明某个陈述是真的，而另一个则拼命想要证明它是假的。在计算机科学的世界里，这被称为量化布尔公式（QBF）。你可以把它看作是一个超级加强版的逻辑谜题，你需要弄清楚，无论你的对手如何应对，是否总有一种获胜的方法。这些谜题极其困难——难到足以驱动从检查自动驾驶汽车软件是否安全，到规划复杂机器人任务的一切领域。几十年来，计算机一直尝试使用一种叫做 DPLL 的方法来解决它们，这就像是一个侦探试图逐一检查豪宅里的每一扇门，直到找到出口。这种方法确实有效，但对于那些最庞大、最纠缠的谜团，侦探会在海量的门面前迷失方向，在找到答案之前就耗尽了时间和精力。

于是，一种名为 CEGAR 的新策略出现了，它的全称是“反例引导的抽象细化”（Counterexample-Guided Abstraction Refinement）。如果说 DPLL 是一个检查每一扇门的侦探，那么 CEGAR 就是一个从豪宅的粗略草图开始工作的侦探。他们先猜想一条路径，如果对手说：“你不能走那里，因为这里有一个特定的陷阱，”侦探并不会放弃。相反，他们会利用这个特定的陷阱（即“反例”）来更新他们的草图，使其更加精确。他们重复这个过程——猜测、得到修正、细化草图——直到草图足够完美，从而无需检查每一扇门就能解开谜团。本文介绍了两种巧妙的方法，利用这种“猜测并细化”的技巧，比以往更快速、更聪明地解决这些逻辑谜题。

作者们是一支来自葡萄牙、爱尔兰和美国的科研团队，他们提出了两种不同的方式，将这种 CEGAR 的魔力引入 QBF 求解器领域。第一种方法是一种全新的求解器，他们将其命名为 RAReQS。RAReQS 并不试图一次性解决整个谜题，也不试图将整个线团展开成一个庞大且难以处理的乱团（这是困扰旧方法的“内存爆炸”问题），而是分层进行游戏。它首先对第一层变量做一个简单的猜测，然后询问一个助手（一个 SAT 求解器）这个猜测是否奏效。如果助手发现了一个缺陷——即对手可以战胜该猜测的一种特定方式——RAReQS 会利用这个缺陷来收紧其对下一次猜测的规则。这就像玩电子游戏时，你不需要看到整张地图，你只需要知道墙在哪里，这样你就不会撞墙。通过只展开那些绝对必要的谜题部分，RAReQS 避免了导致其他求解器崩溃的内存爆炸问题。

第二种方法更像是一种软件升级。作者们采用了现有的、流行的求解器 GhostQ（它使用传统的“检查每一扇门”的 DPLL 方法），并赋予了它一种新的学习工具。他们教会了 GhostQ 使用同样的“猜测并细化”逻辑。当 GhostQ 发现一条看起来不错但最终变成死路的路径时，它不再仅仅是回溯，而是学到了一个深刻的教训：“永远不要再走这条路。”这种新的学习技术让求解器能够更激进地修剪搜索空间，剔除掉那些旧方法会浪费时间去探索的大量不可能出现的场景。

当团队在大量现实世界的逻辑谜题（来自 QBF-LIB 基准测试集）上测试这些新方法时，结果令人瞩目。他们的新求解器 RAReQS 比排名第二的求解器多解决了显著更多的谜题——大约多了 33%。它在与形式验证（检查硬件设计是否正确）和规划（确定机器人的移动方式）相关的题目族中表现尤为出色。对于某些特定类型的谜题，如“增量编码器”（incrementer-encoder）和“红绿灯控制器”（trafficlight-controller），RAReQS 几乎解决了所有的实例，而其他求解器则在挣扎或完全失败。升级后的 GhostQ 也显示出了进步，它比未升级的版本解决了更多的谜题，尽管有时会以牺牲一定的速度或内存使用量为代价。

论文明确指出，虽然这些方法很强大，但它们并不是能瞬间解决一切问题的魔杖。作者指出，如果一个谜题确实需要通过完全展开线团才能解决，那么 RAReQS 可能会做同样多的工作，只是在细化步骤上会有一些额外的开销。然而，对于他们测试的大多数实际问题，这种“部分展开”的策略成为了改变游戏规则的关键。它证明了你不需要看到全貌也能解开谜团；你只需要通过你犯下的错误来不断完善你对重要部分的理解，从而引导你走向真相。这为未来开辟了两条令人兴奋的新路径：构建完全依赖于这种细化循环的求解器，以及教导传统求解器以一种全新的方式从其反例中学习。

技术摘要：利用反例引导细化解决 QBF 问题

问题陈述
量化布尔公式（QBF）将 SAT 问题扩展到了 PSPACE 完全问题，在形式验证和规划领域有着广泛应用。虽然 DPLL 程序在非随机 SAT 求解中占据主导地位，但事实证明它不足以作为 QBF 的通用解决方案。现有的 QBF 求解器通常分为两类：基于 DPLL 的方法和基于展开的方法。基于展开的求解器（如 Quantor、Nenofex）通过将公式展开为命题公式来消除量词，但这往往会导致随着公式规模迅速增长而产生的内存爆炸问题。基于 DPLL 的求解器则在处理 QBF 的搜索空间复杂度方面表现挣扎。本文旨在解决开发更高效的 QBF 求解技术的需求，以减轻内存问题并有效修剪搜索空间。

方法论
作者提出了两种利用反例引导抽象细化（CEGAR）范式的不同方法：

RAReQS（基于递归 CEGAR 的算法）：
- 核心概念： RAReQS 是一种递归算法，它将 QBF 求解视为存在玩家与全称玩家之间的一场博弈。它并不进行完全展开，而是通过反例驱动构建部分展开（抽象）。
- 机制： 算法尝试为公式的一个抽象寻找一个“获胜移动”（即一组变量赋值，使存在玩家满足公式或使全称玩家使公式失效）。
  - 它从空的反例集（ $\omega = \emptyset$ ）开始，代表一个平凡的抽象。
  - 在每次迭代中，它求解当前抽象以找到一个候选获胜移动。
  - 然后，它验证该候选是否为原始公式的获胜移动。此验证过程涉及求解一个子 QBF。
  - 如果该候选验证失败，则生成一个反例（即全称玩家的获胜移动）。
  - 抽象通过将此反例添加到集合 $\omega$ 中进行细化，从而强化抽象以排除失败的候选。
- 优化（多游戏/Multi-games）： 为了解决由于算法递归性（即抽象规模随递归深度呈指数级增长）导致的高内存消耗问题，作者引入了“多游戏”的概念。多游戏允许求解器同时处理多个子公式。抽象被维护为一组子游戏的集合，而细化则是增加新的子游戏而非盲目扩大公式规模。这使得求解器能够在不需要进行完全展开的情况下终止。
- 实现： 该原型使用 C++ 基于 MiniSat 2.2 SAT 求解器实现，支持 QDIMACS 格式。它采用了标准的 QBF 预处理技术，如单位传播和纯文字规则。
作为 DPLL 中学习技术的 CEGAR：
- 核心概念： 该方法将 CEGAR 集成为现有 DPLL 求解器（具体为 GhostQ）中的一种附加学习机制。
- 机制： 当 DPLL 求解器分配变量值使得存在玩家获胜（公式评估为真）时，该赋值被拆分为候选部分（ $\pi_{cand}$ ）和反例部分（ $\pi_{cex}$ ）。
- 学习： 求解器通过修改输入公式来从中学习。如果最后一个决策文字属于获胜玩家，求解器会将相关的量化子公式替换为包含该反例赋值的析取（对于存在量词）或合取（对于全称量词）。具体而言， $\exists X. \Phi$ 被替换为 $(\exists X. \Phi) \lor \Phi[\pi_{cex}]$ ，从而确保在未来的搜索中避免特定的反例赋值。
- 权衡： 该技术允许比标准子句学习更激进地修剪搜索空间，但会带来更高的内存消耗。

主要贡献

RAReQS 算法： 开发了一种新型的、由 CEGAR 驱动的递归 QBF 求解器，通过进行谨慎的、由反例驱动的部分展开，避免了传统展开式求解器固有的内存爆炸问题。
多游戏抽象： 引入了多游戏概念来管理递归 CEGAR 的复杂性和内存使用，使求解器能够高效处理具有任意数量量词层级的公式。
DPLL 中的 CEGAR 学习： 提出了在 DPLL 类 QBF 求解器中利用 CEGAR 作为一种新的学习技术，从而增强搜索空间的修剪能力。
经验验证： 在 QBF-LIB 基准测试集上进行了广泛的实验评估，证明了基于 CEGAR 的技术对于各类问题族都是有效的。

实验结果
作者在来自形式验证和规划领域的 4,669 个 QBF-LIB 实例上评估了原型。

RAReQS 性能： RAReQS 在大量问题族上优于现有求解器（QuBE7.2、Quantor、Nenofex、GhostQ）。它比排名第二的求解器（QuBE7.2）多解决了约 33% 的实例。值得注意的是，RAReQS 解决了 blackbox-01X-QBF 和 trafficlight-controller 等家族的所有实例，并解决了 incrementer-encoder 和 RobotsD2 的几乎所有实例。
内存效率： 在 801 次中止运行中，仅有 50 次是由于内存耗尽导致的，这表明 RAReQS 成功缓解了展开式求解器常见的内存爆炸问题。
DPLL 学习： 将 CEGAR 学习集成到 GhostQ（GhostQ-CEGAR）中通常提高了性能，特别是在 irqlkeapclte（它是唯一找到解的求解器）和 incrementer-encoder 等家族中。然而，在某些家族中，增加的内存开销略微降低了性能。

意义与主张
本文声称开辟了 QBF 求解的两个极具前景的方向：

作为替代方案的 CEGAR 驱动求解器： RAReQS 证明了 CEGAR 驱动的方法可以作为现有 DPLL 和全展开方法的有效替代方案，特别是通过在保持可靠性和完备性的同时，避免了展开式求解器的内存爆炸问题。
DPLL 中的新型学习： 本文确立了 CEGAR 可以有效地作为 DPLL 求解器中的一种附加学习技术，提供比标准子句学习更强大的修剪机制，尽管这需要承担内存成本。

作者总结道，虽然 RAReQS 与展开式求解器有相似之处，但其逐步的、由反例驱动的展开允许它在未能在部分展开中找到获胜移动时提前停止，这是处理大型公式时的关键优势。他们也谦虚地指出，如果最终需要进行完全展开，RAReQS 执行的展开与传统求解器相同，但会带有中间测试的开销。未来的工作包括优化 DPLL 学习以减轻速度损失，并将其他求解器的预处理技术集成到 RAReQS 中。

类似论文