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

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

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

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

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

再看不可行情形

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

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

Disequality 给出另一类边界。约束

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

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

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

现有优化单纯形法公理库单纯形法Simplex method沿可行多面体顶点与边枢轴移动求解线性规划的方法。讨论目标、极点、无界改善与最优证书；本算法借用 pivot 机制，却把状态、终止结果和证书接口改造成 feasibility checking。把 SMT 返回的 SAT 说成“找到了最优解”，或把无界可行域报告为 “unbounded” 失败，都会混淆两个问题。