1 最小满足的基本概念
1.1 布尔变量与逻辑约束
最小满足把问题建立在布尔逻辑之上。通常设定一组布尔变量（取值为“真/假”），并用若干逻辑约束来刻画系统规则。约束常以布尔公式或其等价形式（例如子句集合）给出。对给定变量赋值而言，每个约束要么被满足，要么被违背。最小满足关心的是：在所有可能赋值中，如何让“被满足的约束”尽量多，或让“被违背的约束”尽量少。
这种建模方式的优势在于表达直观：规则之间的冲突不会被简单判定为“可/不可”，而是被量化为“有多少规则不得不让步”。
1.2 满足度与违背度的定义
| 在给定一组约束时，可以用集合大小来度量满足程度。若约束集合为 \(C\)，某个赋值使得其中的子集 \(C_{\text{sat}}\subseteq C\) 被满足，则可定义满足度为 \( | C_{\text{sat}} | \)。与之对应，违背度可以表示为 \( | C | - | C_{\text{sat}} | \)，即不被满足的约束数量。 |
|---|
当所有约束都能被某个赋值同时满足时，违背度为 0；当不存在这样的赋值时，最小满足会寻找使违背度达到尽可能小的赋值，从而度量“离完全一致还差多远”。
1.3 优选目标：最大满足 vs 最小违背
“最小满足”常见两种等价或密切相关的目标表达：
| 1. 最大满足：选择赋值，使被满足的约束数量最大化，即最大化 \( | C_{\text{sat}} | \)。 | ||
|---|---|---|---|---|
| 2. 最小违背：选择赋值，使违背约束数量最小化，即最小化 \( | C | - | C_{\text{sat}} | \)。 |
在约束总数固定的前提下，两者本质上对应同一个最优解：最大化满足数量等价于最小化违背数量。之所以会出现两种表述，是因为不同应用更自然地偏向于“奖励被满足的规则”或“惩罚违背的规则”。
1.4 与完全可满足性的关系（SAT 退化情形）
可满足性问题（SAT）是最小满足的“极端情形”。当存在某个赋值使所有约束都被满足时，最小违背的最优值为 0，此时问题退化为普通 SAT 的可行性判定：要么找到完全满足的赋值，要么证明不存在。
反之，当完全可满足性不存在时，最小满足提供了一个量化结果：它不会止步于“不可满足”，而是回答“至少有多少约束无法同时成立”，从而给出对冲突程度的度量。
2 形式化表述
2.1 子句集合与公式表示
在形式化层面，最小满足通常以子句集合或公式形式给出。一个常见表示是：用一组子句 \(C=\{c_1,\dots,c_m\}\) 构成约束，每个子句由若干文字（变量或其否定）组成。子句集合可以进一步组合成更一般的布尔公式；但从求解与优化角度看，按子句逐一评估其是否被满足是核心操作。
每个子句在某个赋值下的真假状态决定其贡献：被满足则计入目标，违背则产生损失或不计入奖励。
2.2 赋值、真值与满足判定
设变量集合为 \(X=\{x_1,\dots,x_n\}\)。对任意赋值 \(a\)，可把每个变量映射到真或假，从而确定任意文字的真假值。一个子句若至少含有一个文字为真，则该子句整体为真（被满足）；否则子句为假（被违背）。
于是，对于赋值 \(a\)，可以定义满足的子句集合为 \[ C_{\text{sat}}(a)=\{c_i\in C\mid a\models c_i\}, \]
| 其中 \(a\models c_i\) 表示赋值 \(a\) 满足子句 \(c_i\)。目标函数则根据 \( | C_{\text{sat}}(a) | \) 或其补集大小来衡量赋值质量。 |
|---|
2.3 优化形式：目标函数与可行域
最小满足属于优化问题。其基本形式可以写为：在所有可能的赋值空间中寻找最优解。可行域是所有布尔赋值 \(a\in\{0,1\}^n\)。优化目标可以选用最大满足或最小违背。
若采用最大满足形式，可表示为 \[
| \max_{a\in\{0,1\}^n} \ | C_{\text{sat}}(a) | . |
|---|
\] 若采用最小违背形式，可表示为 \[
| \min_{a\in\{0,1\}^n} \ \bigl( | C | - | C_{\text{sat}}(a) | \bigr). |
|---|
\] 两者在子句数量固定时保持一致的最优排序。该框架强调：并不是在“可行/不可行”之间做一次选择，而是在所有赋值上比较“满足程度”。
2.4 加权最小满足
在许多应用中，各约束的重要性并不相同。加权最小满足引入权重 \(w_i\) 表示违背子句的代价或满足的收益。对某赋值 \(a\)，可定义违背代价为 \[ \sum_{c_i\notin C_{\text{sat}}(a)} w_i, \] 并最小化该代价；或等价地最大化被满足的权重和。
这种扩展使模型能够表达“有些规则宁可牺牲，有些规则必须尽量保留”。在资源受限、容错推理等任务中，权重常被用来反映业务优先级、可靠性等级或偏好强度。
3 与经典问题的联系
3.1 与 SAT/Max-SAT 的对偶关系
最小满足与 SAT 的关系体现为“目标极值”的退化：当最优解恰好达到所有约束都被满足的水平时，它等价于 SAT 的可满足性结论。
另一方面，与最大满足（Max-SAT）也存在对应：最大满足本就是最小违背在固定子句数条件下的等价表述。若进一步考虑加权情形，则通常可对应到加权版本的最大满足与最小违背之间的对偶表达。换言之，优化方向不同，但核心比较对象仍是“满足/违背”状态对目标的贡献。
3.2 与约束满足问题（CSP）的对应
约束满足问题（CSP）的一般形式允许变量取多个离散值，并以约束描述变量间关系。最小满足可视为 CSP 的一种“容错”思路：当无法同时满足所有约束时，不直接判失败，而是选择使违反尽可能少的赋值。
在布尔 CSP 的特例中，CSP 的变量域为 \(\{0,1\}\)，其约束可以映射到布尔逻辑子句。此时最小满足可以被看作“带惩罚的 CSP 求解”，把失败实例转化为可度量的最优折中。
3.3 与图论/组合结构的等价建模
许多组合问题能够转化为布尔逻辑形式，从而间接转化为最小满足求解。例如，某些图结构中的冲突选择、覆盖约束或一致性要求，往往可用变量表示是否选择某元素，再用逻辑条件表达合法性。图上的性质冲突会对应到逻辑子句之间的不可同时满足。
在这种等价建模中，最小满足提供一个统一的“冲突最小化”视角：把原问题的硬约束改写为逻辑约束，再通过最优满足程度来度量偏离程度。
3.4 复杂度视角下的分类直观
从复杂度角度看，最小满足通常被视为比普通 SAT 更难处理的范畴，因为它不只是判断是否存在完全满足赋值，还要在所有赋值之间比较最优程度。即使在受限结构下，优化仍需要额外信息或搜索策略。
直观上可以理解为：SAT关心“能否做到全部”，而最小满足关心“做不到全部时，最少让多少”。这种问题通常需要更强的枚举、推断或优化机制。
4 求解方法概览
4.1 穷举与分支定界的思想
最直接的求解思路基于搜索：系统枚举变量赋值，并用上下界剪枝来减少无用分支。分支定界的核心在于将目标值与当前部分赋值的潜力联系起来。例如，当某些变量已被固定后，可以计算在乐观假设下还能满足多少子句；若该乐观上界已经无法超过当前已知最优解，则该分支可以停止探索。
该方法能在小规模或结构较好的实例上取得效果，但在一般情况下仍会面临指数级搜索压力，因此通常需要结合更强的推断与剪枝规则。
4.2 启发式与局部搜索
局部搜索不以“穷尽所有赋值”为目标，而是从某个初始赋值出发，反复执行小幅修改以提升目标。常见做法包括：
- 根据违背子句的统计信息选择变量翻转；
- 使用迭代改进策略逐步减少违背数量；
- 引入随机性或退火式扰动以逃离局部最优。
局部搜索往往对大规模实例更友好，且能快速给出较好解，但其理论最坏情况表现可能不如系统搜索稳定。实践中通常把它作为获得高质量候选解或与其他方法协同的组成部分。
4.3 约束编程与 SAT 求解器的集成思路
约束编程（CP）与 SAT 求解器之间存在天然的协同路径。集成思路通常包括两类：
- 把“最小违背”转化为带控制变量的可满足问题：引入表示某子句是否被允许违背的选择机制，再通过目标优化选择代价更低的方案。
- 使用迭代调用 SAT 求解器：通过不断调整界限（例如当前允许的最大违背数量），逐步逼近最优。
这种做法的价值在于利用成熟的布尔推理与子句学习等技术。虽然具体实现会依赖工具链，但基本原则是把优化目标外显出来，使求解器可以在可满足性框架内完成优化过程。
4.4 近似算法与可行性折中（概念层面）
在某些应用中，允许以较低计算成本换取“足够好”的解。概念上，近似算法会在性能保证或经验表现之间寻求平衡，例如给出满足度相对于最优解的下界，或对违背代价提供可控偏差。
此外，实际系统常采用分层策略：先用启发式快速找到一个可行且较优的解，再用更精细的方法在局部范围内加紧改进。若达到资源限制，则返回当前最优候选。该类折中强调工程可用性：当不能保证找到全局最优时，仍能输出具有明确意义的近似结果。