动机#

前言#

介绍文章前，首先需要说明对于经典的 SMT(QF_NIA)，基于 bit-blasting 做法，简而言之主要是以下三步：

1. 先给整数变量一个有限位宽（bit-width）
2. 把整数运算翻译成位向量电路
3. 再交给 SAT solver

对于第一步而言，一个整数变量 其位向量可以表示为位宽为 的向量 ，其中 为符号位 。

而一个位向量对应的整数值由 计算得出。

然而，如果使用固定位宽的位向量，在整数域上是不完备的

问题#

因此，在基于 bit-blast 的求解方法会带来三个问题：

• 位宽太大，乘法和长加法会产生一个巨大的 CNF，导致 SAT 端压力爆炸
• 位宽太小，搜索空间太窄，会频繁重启甚至根本搜不到解
• 连续加法的结合顺序会影响中间结果位宽，从而影响布尔变量和子句规模

位宽启发式#

乘法自适应位宽#

对于一条带有乘法的约束，我们采用 BMA（Bit-width based on Multiplications Adaptive）来确定，其根据约束中乘法运算的数量（）自适应地确定初始位宽。公式为：

B_{MA} = \max{\beta - \lfloor\alpha m\rfloor, L}

其中， 表示约束中包含的乘法运算数量， 用于调节乘法数量对位宽削减的强度，为 。 表示基础位宽，为 ； 为默认位宽（下限值），默认为

这样可以在乘法较少时尝试较大位宽以提高表达能力，在乘法较多时从小位宽开始以提升求解速度。

唯一图#

我们定义 distinct 图如下：

若某个变量 的度数是 ，那么它至少需要 个不同值候选，因此给出候选位宽为

W_{DG}(x) = \lceil \log_2(deg(x_i) + 1)\rceil

多项式约束#

在多项式约束中，系数与常数项在一定程度上也确定了变量的取值范围：

• 若常数项大，而某变量系数小
• 那么该变量往往需要更大的范围才能抵消常数项

因此我们通过：

W_{CM}(x) = \big\lceil \log_2\left(\frac{\max_i{(|c_i|)}}{|c_x|}\right)\big\rceil + 1

来确定变量 的大概位宽，其中 为系数， 为 x 的系数

截断#

由于前两个启发式可能会给出较大的位宽（例如 ，我们可能会给 很大的位宽）

但是这样会导致生成的电路很大，所以在这里我们进行截断：

W(x) = \min(K, \max(W_{DG}(x), W_{CM}(x)))

而

投票#

最后，我们结合这几个启发式，可以得到一个位宽的候选序列：

B_{VO} = \max(\{w|p(w) \gt \gamma\} \cup \{0\})

其中， 表示位宽 在总位宽设置中所占的比例， 为投票阈值系数， 表示位宽等于 的变量数量，实验中 。

若集合 为空集，则候选位宽 将为 。当 时，我们将把 中所有变量的位宽设置为 与 的最大值。

贪心加#

由于在整数多项式里，大量表达式会形成一长串 successive addition。虽然加法在语义上满足结合律，但在 bit-blasting 成本上不满足：

• (a + b) + c
• a + (b + c)

其中间结果位宽可能不同，因此最终布尔变量和子句数量不同。

我们基于前面的前提，总是优先相加位宽最小的两项，从而最小化 successive addition 过程中中间节点位宽之和，减少布尔变量与子句数，算法如下：

BLAN#

结合后，提出了 BLAN 这个求解器，本质上对 UNSAT 并不完备，这是一个：一个对 SAT 实例 QF_NIA 强的 bit-blasting solver

算法如下所示：