线性实数算术 SMT 的单纯形算法

形式陈述

量词自由线性实数算术的 theory solver 接收线性等式、不等式及其否定。弱不等式的否定仍可写成一个严格反向界，例如 $\neg(x\le c)$ 等价于 $x>c$ ；等式的否定却是

x\ne c\quad\Longleftrightarrow\quad x<c\lor x>c,

不能直接塞成一条 tableau 边界。DPLL(T) 可以让 Boolean 层分裂这个析取，或由 theory solver 暂存 disequality，并在候选赋值命中等号时产生分裂。以下单纯形核心处理完成这些必要分裂后的一组合取。它把每个线性项引入 slack variable，把输入规范化为 tableau 等式

x_i=\sum_{j\in N}a_{ij}x_j \qquad(i\in B)

以及变量界 $l_k\le x_k\le u_k$ ； $B,N$ 分别为 basic 与 nonbasic variables。算法维护一个始终满足全部 tableau 等式的赋值 $\beta$ ，并让 nonbasic variables 处在各自边界内。Basic variable 可以暂时越界，随后通过 pivot 修复。

若 basic variable $x_i$ 低于下界，算法在其行中寻找一个仍能沿正确方向移动的 nonbasic $x_j$ ；高于上界时做对偶选择。“pivotAndUpdate”交换二者角色，把 $x_i$ 放到所需边界并同步更新其余 basic values。若不存在可移动变量，则当前行、 $x_i$ 的违反边界以及阻挡所有方向的 nonbasic bounds 构成不可行证书。把这些活动 theory literals 的否定析取起来，就得到 DPLL(T) 可学习的 theory conflict clause。

本页算法只判定LRA 可满足性。虽然 tableau 和 pivot 来自线性规划，这里没有目标函数、约化成本或最优性判据；输出是一个可行赋值或不可行解释。严格不等式可用符号无穷小 $\delta$ 或等价的精确界表示，不能用任意浮点 epsilon 改写语义。

直觉

“可移动”需同时看系数符号和变量界。若 $x_i$ 低于下界，正系数的 $x_j$ 需要尚未到上界，负系数的 $x_j$ 需要尚未到下界；因为增大前者或减小后者才能抬高 $x_i$ 。选入变量不一定能在自身界内一次修好 $x_i$ ：交换基后它可以成为新的越界基本变量，算法继续修复。真正始终守界的是当前非基本变量。

Tableau 把所有线性关系保持为一张恒真的代数账本，变量界则规定每个数允许落在哪个区间。算法不反复重解方程组，而是让当前赋值沿一条可行方向移动；pivot 改变谁由方程决定、谁可自由贴在边界上。当某个越界 basic variable 想向内移动，却发现行中每个可调变量都已经被相反边界挡住，这一整行就直接解释了矛盾。

上行用 tableau 主元交换把越界的 s=0 修复到绿色 s=2，下行展示 x 与 y 都卡在下界时 s=x+y=2 与 s≤1 形成冲突 — LRA SMT 单纯形的修复与冲突

与优化 simplex 沿目标改善方向找最优顶点不同，SMT 只想找到任意理论模型。可行区域即使无界也已经成功；求解器无须判断目标是否能无限改善。增量接口和冲突 explanation 往往比几何顶点路径更重要。

例子与边界

先看一次可行修复。设 tableau 为 $s=x+y$ ，边界为

s\ge2,\qquad 0\le x\le3,\qquad0\le y\le3.

初始取 nonbasic $x=y=0$ ，等式给出 basic $s=0$ ，违反下界。因为 $x$ 仍可增大，pivot $s$ 与 $x$ ，把 $s$ 设到下界 2；新行写成 $x=s-y$ ，于是 $x=2,y=0,s=2$ ，所有边界均满足。这一步只找到模型，并未优化任何量。

再看不可行情形

x\ge1,\qquad y\ge1,\qquad x+y\le1.

令 $s=x+y$ ，取满足 nonbasic 下界的 $x=y=1$ ，则 tableau 强制 $s=2$ ，违反 $s\le1$ 。要降低 $s$ 只能降低 $x$ 或 $y$ ，二者却已在下界；不存在修复方向。行与三个活动界给出

x\ge1\land y\ge1\land s=x+y \;\Longrightarrow\;s\ge2,

和 $s\le1$ 矛盾。Theory solver 可返回否定这三个输入不等式的子句，Boolean 层随后复用它。

Disequality 给出另一类边界。约束

-1\le x\le1,\qquad x\ne0

可满足，但可行集是 $[-1,0)\cup(0,1]$ ，不是单个闭区间。分裂成 $x<0$ 与 $x>0$ 后，任一分支都可由严格界机制找到模型；若单纯形只满足上下界并返回 $x=0$ ，却忘了最后检查 disequality，这个“模型”并不满足原公式。

严格界可用一个很小的例子检查： $0<x<10^{-12}$ 有解 $x=5\cdot10^{-13}$ 。若用固定 $10^{-6}$ 替代“严格大于”，就会错误报告无解；符号 $\delta$ 表示按字典序比较的形式无穷小，不是提前选定的机器小数。最终提取实数模型时，再依据有限约束选足够小的正值。

退化会让 pivot 不改变数值，错误规则可能循环；终止陈述必须指定精确算术和防循环选择。浮点残差很小也不等于逻辑可行，尤其严格界和相差悬殊的系数会放大误判。整数线性算术还需分支、cut 或其他离散推理，不能把实数 simplex 的模型直接舍入成整数模型。

推论与应用

在 DPLL(T) 中，新增 theory literal 只加入或收紧一个界，旧 tableau 可暖启动；回溯则恢复相应边界。求解器可在 Boolean total assignment 之前发现冲突，也可从界组合推出已登记原子，作为理论传播。Explanation 必须记录原始 literals，而不是只引用会随 pivot 改写的内部行。

现有优化单纯形法讨论目标、极点、无界改善与最优证书；本算法借用 pivot 机制，却把状态、终止结果和证书接口改造成 feasibility checking。把 SMT 返回的 SAT 说成“找到了最优解”，或把无界可行域报告为 “unbounded” 失败，都会混淆两个问题。

参考资料

Bruno Dutertre and Leonardo de Moura, “A Fast Linear-Arithmetic Solver for DPLL(T)”, CAV, LNCS 4144, Springer, 2006, pp. 81–94，§4 的界修复与 §5 的严格不等式。
Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli, “Solving SAT and SAT Modulo Theories,” Journal of the ACM 53(6), 2006, pp. 937–977。
Daniel Kroening and Ofer Strichman, Decision Procedures: An Algorithmic Point of View, 2nd ed., Springer, 2016，线性算术部分。

形式陈述 ​

反向链接

形式陈述