在让AI思考之前，先清理它的输入

逻辑公式和推理查询并非同一回事，但在许多AI流程中，它们紧密相伴：以合取范式（CNF）表示的知识库被编译成紧凑的电路，而该电路则回答关于其模型的问题。几十年来，从业者一直在争论是否应该先对CNF进行预处理，以及哪些简化是安全的。一项由CRIL（法国国家科学研究中心与阿尔托大学联合实验室）研究人员发表的研究给出了明确的答案：保留模型计数并同时保留被消除变量定义的预处理器，能带来显著的性能提升；而仅保留可满足性的预处理器，对采样和枚举毫无用处。

预处理全景

这篇由Jean Marie Lagniez和Emmanuel Lonca主导的论文，考察了三类预处理技术：保留逻辑等价性（活化、骨干检测、约减出现）、仅保留可满足性（变量消除、阻塞子句消除），以及通过移除已定义变量来保留模型计数的方法。对于均匀采样、直接访问（按字典序返回第k个模型）和模型枚举等任务，区别至关重要。

作者证明，变量消除和阻塞子句消除等仅保留可满足性的技术，与这些查询从根本上不兼容。在一个简单的反例中，公式a ∨ b在两种方法下均被约简为⊤，丢失了所有关于原始模型的信息。他们写道：“从Φ'无法恢复Φ的模型”，这证实了模型计数领域一个已知的局限性。

更令人惊讶的是发现，即使是保留模型计数的技术（消除由其他变量隐式或显式定义的变量）也不能直接应用。预处理后的公式本身缺乏重建原始模型所需的映射。然而，当被消除变量的定义存储在一个兼容的求值函数中时，该方法对均匀采样和完整模型枚举就变得可行。

直接访问要求排序

直接访问查询（用户请求特定字典序变量顺序下的第k个模型）增加了一个额外约束。作者定义了一种“兼容顺序”，将所有被消除变量放在其定义变量之后。这保证了预处理公式的第k个模型，在通过求值函数扩展后，与原始的第k个模型完全对应。出现了两种策略：要么预处理步骤固定变量顺序的尾部，要么将消除限制在其定义变量全部出现在给定顺序更早位置的变量上。前一种消除更多变量；后一种则赋予用户完全自由。

部分模型枚举是该方法遭遇硬性限制的领域。研究人员展示了一个例子：消除由异或门定义的变量会导致原始和简化公式中部分模型数量之间存在指数差距；奇偶函数没有紧凑的表示，因此预处理实际上破坏了部分枚举所需的结构。

来自1,425个基准的实验证据

团队使用B+E预处理器和d4知识编译器，在以往均匀采样研究的基准上进行了广泛实验。他们测试了四种配置：无预处理、仅等价性保留（equiv）、等价性加显式定义变量消除（#equiv-explicit）、以及在此基础上施加兼容顺序（#equiv-explicit-ordered）。

仙人掌图显示出一个清晰的层次。仅equiv预处理带来的收益很微弱，只比无预处理多解决了8个实例。#equiv-explicit-ordered比基线多处理了47个实例，这是一个显著的改进；而#equiv-explicit甚至多解决了55个，但如果没有排序约束，它无法直接回答直接访问查询。对于均匀采样和枚举，作者报告了显著的运行时间缩减，预处理后的电路始终优于其原始版本。

这项工作为AI工程师强调了一个实用原则：如果下游任务涉及模型计数、采样或枚举，应投资于保留模型计数并向前传递变量定义的预处理器。与节省的编译时间相比，跟踪这些定义的开销微乎其微。