切割平面证明系统

归结一次只消去一对相反文字，切割平面则把许多布尔约束放进同一个算术账本。线性组合像把几张“至少需要多少资源”的清单相加；rounding rule 使用变量必须取整数这一信息，从线性松弛的分数边界切掉不含整数点的一层。这与线性规划公理库线性规划Linear programming · LP在线性等式和不等式约束下优化线性目标函数的问题。中的半空间推理相似，但证明目标不是优化，而是展示所有布尔点都被排除。

取整是系统真正超出纯实数线性推理的地方。由 $2x\ge 1$，实数语义只能得 $x\ge \frac{1}{2}$；整数语义却得 $x\ge 1$。多次组合和取整可以压缩基数、鸽巢与计数论证。然而系数可能迅速增长，所以“行数少”并不保证证书比特数小；证明复杂度必须把整数的二进制长度算进去。

考虑不可满足公式

前三个子句要求每一对变量之和至少为 $1$；后三个要求每一对之和至多为 $1$。把前三个不等式相加得到

除以 $2$ 并把 $3/2$ 向上取整，得到 $x+y+z\ge 2$。后三式的线性编码分别为 $-x-y\ge -1$、$-x-z\ge -1$、$-y-z\ge -1$；相加、除以 $2$ 并取 $\lceil -3/2\rceil =-1$，得到 $-x-y-z\ge -1$，也就是 $x+y+z\le 1$。两条结论相加即为 $0\ge 1$。分数点 $x=y=z=\frac{1}{2}$ 满足原来的全部六个线性不等式，所以实数松弛确实可行；正是两次整数取整删掉了这个分数点并暴露矛盾。

规则的精确形式不可省略。“把所有系数随意取整”通常不保真；上述除法要求左侧可整体除以同一正整数，再只对右端做 ceiling。允许有理系数时可先清分母，但清分母的位数也属于证明大小。若系数用一元编码与二进制编码，所谓多项式长度可能不同，引用下界前必须核对模型。

切割平面处理的是布尔整数不等式。对一般整数规划的 Gomory cuts、Chvátal–Gomory rank 或加入乘法的系统，规则集和资源度量都更强，不能都简称为同一个 CP。证明中出现一个很大的系数也不等于表达了同样大的逻辑信息；其来源必须由合法组合逐行认证。

切割平面能自然表达基数与计数论证。例如鸽巢原理公理库鸽巢原理Pigeonhole principle · Dirichlet's box principle把多于 n 个对象放入 n 个容器时，至少一个容器包含两个对象。的“每只鸽子至少进一个洞”和“每个洞至多一只鸽子”直接成为线性不等式，整体求和即可暴露容量冲突；但不同鸽巢编码和 CP 变体的证明长度仍需逐一分析。CP p-模拟标准 resolution，因为每个子句已有线性编码，归结步骤可由少量加法和必要取整实现；这个方向不意味着已知反向多项式模拟。

证书检查还揭示一个实用优势：验证者不必重新求解原整数规划，只需重算每行的系数向量、检查乘子非负，并核对共同除数和 ceiling。若第 $i$ 行含 $n$ 个二进制整数，单步成本对这些整数的总位数为多项式；因此系数增长虽然会拉长证书，却不会暗中调用一个整数规划 oracle。

下界研究常把 CP 证明变成通信协议、单调电路或几何切割过程。可行插值公理库可行插值Feasible interpolation · Feasible Craig interpolation从分割变量的短命题证明中以多项式开销提取只依赖共享变量的分离电路。尤其能从某些短 CP 证明提取分离电路，再借电路下界反推证明下界。不过“CP 具有插值”必须说明所用规则、系数界和是否要求单调插值；对任意增强版系统不能无条件沿用。