使用 BEE 将有限域约束编译为 SAT：导演剪辑版

BEE 是一个编译器，通过将有限域约束编码为合取范式（CNF）并应用底层 SAT 求解器来促进其求解。在 BEE 中，约束被建模为布尔函数，用于传播关于布尔文字之间相等性的信息。随后应用这些信息来简化约束的 CNF 编码。我们将此过程称为等值传播（equi-propagation）。一个关键因素是，一次仅考虑约束模型的一小部分，使得能够应用更强甚至完全的推理来检测该部分中的等价文字。一旦检测到等价性，它们就会传播以简化整个约束模型，并促进对其他部分的进一步推理。BEE 已在最近的几篇论文中进行了描述。在本文中，在快速回顾 BEE 之后，我们详细阐述了实现中两个未记录的细节：基数约束的混合编码和完全等值传播。接着，我们描述了旨在扩展 BEE 以考虑数字二进制表示的正在进行的工作。