💻 computer science

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses

本文介绍了两种新型求解器 tabularAllSAT 和 tabularAllSMT，它们利用带有时序回溯的冲突驱动子句学习以及激进的蕴涵项缩减算法，在不依赖阻塞子句的情况下，高效地枚举 SAT 和 SMT 问题的不相交满足赋值。

原作者： Giuseppe Spallitta, Roberto Sebastiani, Armin Biere

发布于 2026-05-11

📖 1 分钟阅读☕ 轻松阅读

原作者： Giuseppe Spallitta, Roberto Sebastiani, Armin Biere

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

想象你是一名侦探，试图找出能解开一个庞大而复杂谜案的所有可能的线索组合。在计算机科学领域，这个“谜案”就是一个逻辑公式，而“线索”则是各种变量的真/假设置。这项任务被称为AllSAT（寻找所有解）或AllSMT（当线索涉及数学或其他复杂规则时寻找所有解）。

你提供的这篇论文介绍了两种新工具：TabularAllSAT和TabularAllSMT，旨在比以往的方法更快、更高效地完成这项侦探工作。以下是通过简单类比对它们工作原理的解释。

问题：“阻断”瓶颈

传统上，当计算机找到一个谜题的解时，它需要确保不会再次找到完全相同的解。

旧方法（阻断子句）： 想象侦探找到了一个解，将其记录下来，然后在该特定路径上挂起一个巨大的“禁止进入”标志（即阻断子句）。接着，他们回到起点重新开始。
- 缺陷： 如果存在数百万个解，侦探最终会用数百万个“禁止进入”标志覆盖整张地图。最终，地图被标志 clutter 得如此混乱，以至于侦探感到困惑、速度变慢，并且没有足够的空间写下所有这些标志。这就是论文中提到的“内存爆炸”。

解决方案：“按时间顺序”的行走

作者提出了一种更聪明的方式来遍历谜题，而无需那些“禁止进入”标志。

新方法（按时间顺序回溯）： 侦探不再竖起标志，而是系统地遍历谜题。当他们遇到死胡同或找到一个解时，只需退后一步回到他们所做的最后一个决定，翻转该决定（就像将开关从“开”拨到“关”），然后继续前行。
- 优势： 因为他们按照严格、有序的顺序行走（就像逐页阅读一本书），他们自然地不会两次访问同一个位置。无需标志，地图保持整洁，侦探也永远不会因杂乱而不知所措。

“缩减”技巧：寻找核心

一旦侦探找到了一个完整解（其中每个线索都有一个值），他们意识到实际上并不需要所有线索来证明该解有效。也许 10 个线索中只有 3 个是关键的，其余 7 个可以是任意值。

旧缩减法： 以往的方法非常谨慎。他们只有在绝对确定安全时才会移除线索，这往往会在解中留下多余的“死重”。
新的“激进”缩减法： 作者创建了一种新算法，其作用如同一个无情的编辑。它会审视解并问道：“移除这个线索会破坏逻辑吗？”如果是，它会立即将其剔除。
- 结果： 计算机不再返回包含 10 个线索的冗长混乱列表，而是返回一个仅包含 3 个关键线索的微小、紧凑列表。这极大地减少了计算机需要处理和存储的数据量。

处理“重要”与“不重要”变量（投影）

有时，侦探只关心特定的线索（例如，“谁偷了饼干？”），而不关心其他线索（例如，“天空是什么颜色的？”）。

挑战： 如果计算机在求解整个谜题时包含了天空颜色，就会浪费时间。
对策： 新工具被教导要优先考虑“重要”线索。它们求解谜题，但完全忽略“不重要”的线索。这就像解决迷宫时只关心通往出口的路径，而不关心墙上的装饰。这使得搜索速度大大加快。

处理数学和复杂规则（SMT）

到目前为止，我们讨论的是简单的真/假开关。但现实世界的问题往往涉及数学（例如"x + y > 10"）。

扩展： 作者升级了他们的侦探以处理这些数学规则。他们在团队中加入了一位“数学顾问”（理论求解器）。
- 当侦探做出猜测时，他们会询问数学顾问：“这符合数学规则吗？”
- 如果数学说“不”，侦探会立即退后并尝试另一条路径，而不是浪费时间走上一条数学上不可能通行的路径。

核心结论

论文声称，通过将严格有序的行走方式（按时间顺序回溯）与无情的编辑风格（激进缩减）相结合，他们的新工具（TabularAllSAT和TabularAllSMT）比当前最佳工具更快且占用内存更少。

它们不会被“禁止进入”标志所** clutter**。
它们通过剔除不必要的细节，返回更小、更清晰的解。
它们能够处理复杂数学而不会陷入困境。

作者将这些工具与最佳竞争对手进行了测试，发现他们的方法解决了更多问题，速度更快，尤其是在问题规模巨大或涉及复杂数学时。

技术摘要：无需阻塞子句的 SAT 与 SMT 不相交投影枚举

问题陈述

本文探讨了**全解可满足性（AllSAT）及其扩展全解理论可满足性（AllSMT）**固有的计算挑战。其目标是枚举公式的所有满足赋值。虽然传统 SAT 求解器在找到一个解后即终止，但枚举需要探索整个搜索空间。

主要识别出两个困难：

指数级搜索空间：对于具有 $n$ 个变量的公式，存在 $2^n$ 种可能的完整赋值。对于较大的 $n$ ，显式枚举是不可行的。本文主张使用部分赋值（蕴含项）来表示完整赋值的集合，从而压缩解空间。
阻塞子句与内存：基于冲突驱动子句学习（CDCL）和非时序回溯（NCB）的传统 AllSAT 求解器依赖于添加阻塞子句以防止重新发现相同的模型。随着模型数量的增长，阻塞子句的数量可能呈指数级增加，导致内存爆炸并降低单元传播性能。
投影：在许多应用中（例如通过 Tseitin 变换转换非 CNF 公式），只需枚举“重要”变量（ $V_r$ ）子集的解，而忽略辅助的“无关”变量（ $V_i$ ）。

本文专注于不相交枚举，其中严格禁止重复的赋值，这是加权模型积分（WMI）和概率推理等应用的要求。

方法论

作者提出了两种新型求解器：TabularAllSAT（用于命题逻辑）和TabularAllSMT（用于 SMT）。两者均将CDCL与**时序回溯（CB）**相结合，以消除对阻塞子句的需求，同时保持不相交性。

1. 核心搜索算法（CDCL + CB）

搜索循环结合了 CDCL（通过冲突分析逃离不可满足区域）和 CB（无需冗余阻塞子句进行系统探索）的优势。

冲突处理：当检测到冲突时，求解器执行标准的冲突分析以推导出冲突子句。然而，求解器不像标准 CDCL 那样非时序地跳回到冲突子句所在的层级，而是时序地回溯到最近分配的决策文字并翻转其值。
隐式阻塞：为了确保在不存储显式阻塞子句的情况下实现不相交性，求解器利用虚拟回溯原因子句。当找到一个模型并翻转一个决策文字时，翻转的原因被记录为 Backtrue。这隐式地定义了一个阻塞子句，该子句由直到该点的所有决策文字的否定组成。
终止：当求解器回溯到决策层级 0 时，搜索终止，确保整个空间已被系统扫描且无重复。

2. 时序蕴含项收缩

一个关键组件是将完整赋值缩减为紧凑的部分赋值（蕴含项）。本文介绍了两种算法：

保守收缩（基线）：基于 2-监视文字，该算法检查某个文字对于当前部分赋值满足公式是否必要。它尊重决策顺序和 Backtrue 标志以确保不相交性。
激进收缩（新颖）：该算法模拟最优决策顺序。它识别“必要”文字（满足特定子句所需的文字）和“不必要”文字。只要文字未被标记为 Backtrue 或未参与冲突分析，无论其决策层级如何，都允许移除不必要文字。这是通过以下方式实现的：
1. 计算每个子句中当前在路径（trail）中的文字数量。
2. 迭代移除不是任何子句唯一满足者的文字。
3. 仅用必要文字重建路径，有效地将不必要变量的赋值推迟到搜索循环的末尾。

3. 投影与 SMT 的扩展

投影枚举：算法被调整以处理相关变量（ $V_r$ ）的子集。决策启发式优先选择 $V_r$ 而非无关变量（ $V_i$ ）。在蕴含项收缩期间，对应于 $V_i$ 的文字被自动丢弃，确保输出仅包含 $V_r$ 的赋值。
AllSMT 集成：该框架集成了理论求解器（MathSAT5）。搜索循环在单元传播后包含T-一致性检查。如果发生理论冲突，则像布尔冲突一样进行分析，求解器进行时序回溯。求解过程中生成的理论原子在投影目的上被视为无关变量。

主要贡献

本文概述了五项主要贡献：

不相交部分枚举：一种结合 CDCL 和时序回溯的过程，用于在不引入阻塞子句的情况下枚举不相交的部分模型。
蕴含项收缩算法：两种算法（保守和激进），旨在最小化部分赋值，同时严格遵守底层演算的不相交性约束。
投影枚举扩展：求解器的适配，仅枚举重要变量的子集，处理 CNF 变换中引入的辅助变量。
SMT 扩展：将理论推理集成到枚举框架中，实现具有不相交部分枚举的 AllSMT 求解。
实验评估：与最先进求解器的全面基准测试。

实验结果

作者在各种基准测试（随机 3-SAT、SATLIB、合成 SMT 和非 CNF 公式）上评估了TabularAllSAT和TabularAllSMT，对比的求解器包括 MathSAT5、Dualiza、基于 BDD 的求解器以及 D4+ModelGraph。

蕴含项收缩：与保守基线相比，新颖的激进收缩算法显著减少了生成的部分赋值数量，特别是在具有大量完整解的实例上。虽然在非常小的实例上产生了轻微开销，但它改善了较大问题的整体执行时间。
AllSAT 性能：TabularAllSAT 的表现与大多数求解器（BC、NBC、MathSAT5）相当或更优。在子句较少且编译开销较低的特定基准测试中，它被知识编译工具（BDD、D4+ModelGraph）超越。然而，TabularAllSAT 展示了更低的内存占用，并且没有因内存耗尽而超时。
投影 AllSAT：在需要投影的非 CNF 基准测试上，TabularAllSAT 在速度和解决的实例数量方面显著优于 MathSAT5 和 Dualiza。在更难的合成基准测试上，它也超越了 D4+ModelGraph。
AllSMT 性能：TabularAllSMT 在完整枚举和部分枚举任务中均优于 MathSAT5（唯一其他可用的投影 AllSMT 求解器）。TabularAllSMT 中缺乏阻塞子句，避免了 MathSAT5 随着问题复杂度增加而观察到的性能下降。

意义与主张

本文声称，所提出的方法提供了一种优于传统基于阻塞子句枚举的替代方案，特别是在需要投影和 SMT 推理的场景中。

效率：通过避免阻塞子句的指数级增长，求解器保持了稳定的单元传播性能并避免了内存爆炸。
紧凑性：激进的蕴含项收缩算法产生更紧凑的部分赋值，减少了输出大小和后续枚举步骤的搜索空间。
通用性：该框架成功统一了命题和基于理论的枚举的 CDCL 与时序回溯，将不相交枚举的适用性扩展到概率推理和一阶理论上的模型计数等复杂领域。

作者将其工作定位为形式演算 [17] 的实际实现，提供了首个有效处理投影和 SMT 而无需阻塞子句开销的实现。