SAT（Satisfiability Problem）是判定逻辑命题是否存在一种变量赋值使得整个逻辑表达式为真的问题。通常用布尔逻辑表达式表示，目标是找出一组变量的真/假值，使得表达式为真。
混合整数线性规划问题是一类优化问题，其目标函数和约束条件都是线性的，决策变量可以包含整数变量和联系变量。
简单的来理解就是SAT问题是混合整数线性规划问题的一个子集。那么SAT问题和混合整数线性规划问它们之间的区别主要有以下几个方面：
1 变量类型的区别
SAT 问题只有布尔变量，在SAT问题里边任意一个变量只有 true 或者 fasle 两个可以选择的取值。也就是说 SAT 问题里边不能包括 非布尔变量的 整数变量 和 连续变量。
显然，对于混合整数线性规划问题而言，决策变量可以是布尔变量，也可以是一般的整数变量，也可以包括连续变量。
2 约束类型的区别
SAT问题的约束只有一种类型就是 若干个布尔变量 与或非运算之后，得到的结果为 true 和 false，例如对于约束
其中 都是布尔变量。上面这个约束采用SAT里边逻辑表达式如下所述：
但是我们发现如果约束是小于等于1的时候：
我们依然可以非常方便的采用混合整数线性规划来建模，但如果采用逻辑表达式来表达就会显得稍微复杂一点，如下所示：
上面的表达式包含了三个逻辑子句，也就是在混合整数线性规划中一条约束可能会对应到SAT问题里边是很多条子句（子句就是SAT问题中的约束）。
3 目标函数的区别
SAT问题通常是找到一个满足约束的解即可，也就是说获取可行解即可，没有目标函数。而混合整数线性规划问题，大多数情况下是包括最大化或者最小化目标函数的。这一点可以说是SAT问题和混合整数线性规划问题的重要区别。
4 求解算法的区别
SAT问题的研究主要是在理论计算机领域，而混合整数线性规划主要是在运筹学领域，虽然我们看到这两类问题有很强的关联，但不同的社区会导致其在求解思路上存在一定的差异性。
SAT问题中常用的算法是 CDCL算法（Conflict-Driven Clause Learning），这些算法使用剪枝、冲突学习等技术以提高求解效率。
混合整数线性规划常用的求解算法是分支定界法（Branch and Bound），由于混合整数规划问题的复杂性，MILP求解器依赖于高级的剪枝策略、启发式方法以及有效的松弛求解。
当然实际上现代的混合整数线性规划求解器例如Gurobi等，已经大量的借鉴和吸收了很多SAT问题的高效算法，例如 domain propagation 算法，例如 conflict detection 等技术。这两个社区有一定的不同，但也在逐步地互相学习，一些很有意义的交叉性研究也在开展。
5 总结
| 特点 | SAT问题 | 混合整数线性规划问题（MILP） |
|---|---|---|
| 变量类型 | 布尔变量（0或1） | 整数和连续变量 |
| 目标 | 找到满足逻辑表达式的赋值 | 最小化或最大化线性目标函数 |
| 表达形式 | 布尔逻辑表达式 | 线性约束和线性目标函数 |
| 求解方法 | DPLL、CDCL | 分支定界、分支切割 |
| 应用领域 | 逻辑验证、组合优化 | 资源分配、生产规划、物流优化 |
微信公众号后台回复
加群：加入全球华人OR|AI|DS社区硕博微信学术群
资料：免费获得大量运筹学相关学习资料
人才库：加入运筹精英人才库，获得独家职位推荐
电子书：免费获取平台小编独家创作的优化理论、运筹实践和数据科学电子书，持续更新中ing...
加入我们：加入「运筹OR帷幄」，参与内容创作平台运营
知识星球：加入「运筹OR帷幄」数据算法社区，免费参与每周「领读计划」、「行业inTalk」、「OR会客厅」等直播活动，与数百位签约大V进行在线交流
文章须知
微信编辑：疑疑
关注我们
FOLLOW US
