Improving Bit-Blasting for Nonlinear Integer Constraints

动机

前言

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

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

对于第一步而言，一个整数变量 $x$ 其位向量可以表示为位宽为 $w$ 的向量 $\bar{x}:<{\bar{x}}_{w-1},\cdots ,{\bar{x}}_1,{\bar{x}}_0>$，其中 ${\bar{x}}_{w-1}$ 为符号位 。

而一个位向量对应的整数值由 $val(\bar{x})=-2^{w-1}\times Int({\bar{x}}_{w-1})+2^{w-2}\times Int({\bar{x}}_{w-2})+\cdots +{\bar{x}}_0$ 计算得出。

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

Example

对于约束 $x+y=z$ 而言，假定现在所有变量的位宽都为 $2$，那么在 QF_BV 中，$val(\bar{z})\in [-2,1]$，这是因为我们完全没有考虑溢出的情况，如果用位宽为 $3$ 的向量来表示，就可以表示出 $-2+(-2)=-4$，而不是 $-2+(-2)=<1,0>+<1,0>=<0,0>=0$

Search Box

每个整数变量都映射到一个有限闭区间 $[l,u]$，我们称为 search box，其决定了 bit-blasting 时的搜索空间。

问题

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

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

位宽启发式

乘法自适应位宽

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

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

其中，$m$ 表示约束中包含的乘法运算数量，$\alpha \in {\mathbb{R}}^{+}$ 用于调节乘法数量对位宽削减的强度，为 $1536$。$\beta \in {\mathbb{Z}}^{+}$ 表示基础位宽，为 $7$；$L$ 为默认位宽（下限值），默认为 $2$

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

唯一图

我们定义 distinct 图如下：

Distinct Graph

给定图 $G=<V,E>$ ，其中 $V=\{x_1,\cdots ,x_n\},E=\{(x_i,x_j)|x_i,x_j\in V\wedge x_i\ne x_j\in \psi \}$ ，其中 $\psi$ 为一条形如 $(distinct{x}_1,x_2,\cdots ,x_i)$ 的约束 (all-different)

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

$$W_{DG}(x)=\lceil {\log }_2(deg(x_i)+1)\rceil$$

多项式约束

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

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

因此我们通过：

$$W_{CM}(x)=\lceil {\log }_2\left(\frac{{\max }_i(|c_i|)}{|c_x|}\right)\rceil +1$$

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

截断

由于前两个启发式可能会给出较大的位宽（例如 $x^2\ge 1\vee y\ge 1000$，我们可能会给 $y$ 很大的位宽）

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

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

而 $K=16$

投票

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

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

其中，$p(w)=\frac{♯(W(x)=w)}{|{\mathcal{V}}_{int}|},x\in {\mathcal{V}}_{int}$ $p(w)$ 表示位宽 $w$ 在总位宽设置中所占的比例，$\gamma \in (0,1)$ 为投票阈值系数，$♯(W(x)=w)$ 表示位宽等于 $w$ 的变量数量，实验中 $\gamma =0.5$。

若集合$\{w|p(w)>\gamma \}$ 为空集，则候选位宽 $B_{VO}$ 将为 $\{0\}$。当 $B_{Vote}\ne \{0\}$ 时，我们将把 ${\mathcal{V}}_{int}$ 中所有变量的位宽设置为 $B_{MA}$ 与 $B_{VO}$ 的最大值。

贪心加

Info

总是优先相加当前 bit-width 最小的两个项

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

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

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

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

BLAN

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

算法如下所示：