不可行性分析与约束放宽

不可行性分析回答“为什么没有任何方案满足条件”。它与临界约束自动分析共享诊断方法，但后者通常在可行模型上增加更优目标，再解释目标为什么不可达。

1. 先区分问题来源

输入缺失、单位错误、变量域误设和真实业务矛盾都可能表现为无解。先确认输入与表达符合业务，再分析冲突。超时没有找到解不是不可行证明，后端不支持也不是业务矛盾。

一个冲突只说明特定模型中的条件不能同时成立，不证明其中某条规则本身错误。是否能放宽由业务性质和授权决定。

2. 例子：需求超过内部产能

概述、概念与变量

单期生产上下文必须满足需求 $D=10$ 件，但内部容量为 $K=8$ 件。变量 $x\in {\mathbb{Z}}_{\ge 0}$ 是内部产量。没有辅助变量或筛选谓词；交付量中间值 $Q=x$。

断言与约束

需求和容量为非负整数是输入断言。业务约束为：

$$c_D:Q\ge 10,c_K:x\le 8.$$

这里是满足性诊断，不需要优化目标。背景 $B$ 保留非负整数域。

解释

$c_D$ 和 $c_K$ 不能同时成立。删去需求条件，$x=0$ 可行；删去容量条件，$x=10$ 可行。因此它们形成相对于 $B$ 的一个按包含关系极小冲突。

这并不意味着容量数据应改为 10，也不意味着可以少交 2 件；它只解释现有条件的不相容。

3. 冲突、IIS 与 MUS

冲突集合是足以导致不可行的一组条件，不一定极小。MUS 表示按包含关系不可再删的不可满足子集；IIS 常用于数学规划中的不可约不可行子系统，可能包含约束行和变量界。

极小不等于数量最少，不保证唯一。以求解器行得到的 IIS 映射成业务名字后，也不自动成为业务约束层面的 MUS。拆分一条业务规则或合并一组实例，会改变诊断粒度。

令 $M$ 为待解释约束，背景为 $B$，其极小性含义是：

$$B\wedge \underset{c\in M}{\bigwedge }c\text{ 不可满足},$$$$\mathrm{\forall }c\in M,B\wedge \underset{d\in M\setminus \{c\}}{\bigwedge }d\text{ 可满足}.$$

重复满足性求解中遇到未知，只能保留未确认的极小性，不能把超时当成不可满足。

4. 原始证据与不可放宽背景

业务报告使用规则身份、变量界、离散域及实例索引。辅助变量和转换生成行可以用于内部定位，但最终应回到业务定义。

背景包括始终保留的条件。若背景自身不可行，单纯在可调整候选中找修正集合无法解决问题。法律、安全或物理规则可能属于背景，但“不可放宽”的分类需要明确来源，不由算法任意猜测。

5. 从诊断到放宽模型

允许的业务修改

假设容量本身不允许虚增，但业务允许加班生产最多 1 件，并外协最多 2 件。增加变量 $h\in \{0,1\}$、$o\in \{0,1,2\}$，单位件；它们分别表示额外容量和外协数量。

交付量与追加成本为：

$$Q=x+o,C=3h+5o.$$

限制内部生产 $0\le x\le 8+h$，满足需求 $Q\ge 10$，最小化 $C$。数据断言是加班和外协上限确实可用。这不是删除原始规则，而是明确改变资源来源。

结果与边界

选择 $h=1,o=1,x=9$，成本为 8；不用加班则需要 $o=2$，成本为 10。因此最优追加成本为 8。

诊断解释“缺 2 件容量”，放宽模型回答“在允许的选项中怎样补足”。如果这些选项尚未批准，结果只是建议，不是正式执行方案。

6. 修正集合与松弛量

极小修正集合（MCS）是从完整模型移除后可恢复可行、且移除集合不能再缩减的一组允许修改条件。它不是冲突集合本身。一个冲突被解除后，其他冲突仍可能存在。

对可量化约束可引入松弛量并惩罚，但各项单位和代价必须明确。降低需求、增加容量和允许迟交不是同一业务动作，不能仅因数学上都能引入 slack 就混用。

7. 在 OSPF 中组织诊断

分析使用独立模型或快照，临时停用和放宽不写回原业务定义。上下文维护稳定的约束和分组身份，应用负责选择背景、候选和允许的修改范围，后端提供它能支持的冲突或满足性信息。

报告同时展示冲突、背景、诊断粒度和未知状态。多组解释可以并列，不能把第一组当成唯一原因。进一步阅读多目标与软约束和场景分析。