面向有效基化的提升单元传播

公式 $\phi$ 在给定有限域上的基化是一个在该域上与 $\phi$ 等价的基础公式。高效的命题求解器使得基于基化的问题求解方法日益重要，然而对于现实问题域和实例，基化规模往往存在问题。基础求解器（如 SAT 求解器）中的一项关键技术是单元传播，它通常能在搜索开始前就显著缩减基础公式的规模。我们定义了一种可在基化之前执行的“提升”版单元传播，并描述了将该技术集成到基化算法中的方法。我们阐述了该方法在一个自底向上基化器中的实现，并对其性能进行了实验研究。