Composer使用SAT求解器将依赖关系转化为逻辑命题，通过全局分析所有版本约束与冲突，精确找出可行解或明确报告无解原因，避免传统递归方法的局限，提升复杂项目依赖解析的可靠性与准确性。
Composer 的依赖解析器使用一种基于布尔可满足性问题（SAT solver）的技术来解决复杂的依赖关系。它并不像传统递归方式那样逐层安装包，而是将整个依赖图转化为一个逻辑命题公式，然后通过 SAT 求解器判断是否存在一组能满足所有约束的包版本组合。
什么是 SAT Solver？
SAT（Satisfiability）求解器用于判断一组布尔变量是否存在某种赋值方式，使得给定的逻辑表达式为真。在 Composer 中，这个机制被用来建模 PHP 包之间的依赖、冲突和版本约束。
例如，当你要求安装 package-a ^2.0，而它依赖 package-b >=1.5，同时另一个已安装的包冲突 package-b 1.6，那么这些规则会被转换成逻辑子句，由 SAT 求解器分析是否能找出兼容的解决方案。
Composer 如何使用 SAT 求解依赖？
Composer 将每个包的每个版本视为一个“原子命题”，然后构建以下类型的规则：
- 依赖规则：如果选择了 package-a 2.1，则必须选择满足 package-b >=1.5 的某个版本
- 互斥规则：同一个包的不同版本不能共存（如 package-a 2.1 和 2.2 不可同时选）
- 冲突规则：某些包或版本明确声明了冲突（conflict 字段）
- 推荐/建议：非强制，但会影响优先级选择
所有这些规则被编译成合取范式（CNF），输入给内部的 SAT 求解器（基于 minisat 或类似算法变种）。求解器尝试找出一组“启用哪些包版本”的布尔赋值，使整体公式成立。
为什么用 SAT 而不是简单递归？
传统的依赖解析方法容易陷入局部最优或无法回溯，尤其在存在多重依赖路径和版本冲突时。SAT 求解器的优势在于：
- 全局视角：一次性考虑所有可用版本和约束
- 高效回溯：当某条路径失败时，能快速排除大片无效组合
- 精确求解：要么找到可行解，要么确定无解，并给出冲突原因
这使得 Composer 可以准确报告“无法安装”并提示具体是哪几个包导致冲突，而不是中途报错退出。
实际表现与优化
虽然 SAT 是 NP 完全问题，但 Composer 做了许多优化来提升性能：
- 版本范围预处理：把语义化版本约束转换为具体的包版本列表
- 缓存已知结果：避免重复计算相同的依赖场景
- 剪枝策略：提前排除明显不兼容的版本组合
尽管如此，在极端情况下（如大量包且约束复杂），解析仍可能较慢，这也是为什么有时会看到 “Resolving dependencies with SAT” 耗时较长。
基本上就这些。Composer 的 SAT 解析器让依赖管理更可靠，尤其在大型项目中能有效避免“依赖地狱”。
