Composer使用SAT求解器解决PHP依赖管理问题，将包版本选择转化为布尔逻辑表达式，通过合取范式（CNF）描述依赖、冲突和互斥规则，调用picosat高效求解。相比传统递归回溯，SAT方法具备完整性、高效剪枝和强逻辑表达能力，能系统探索所有可能组合，避免遗漏可行解，提升复杂依赖解析的可靠性与效率。
Composer 是 PHP 的依赖管理工具，它能自动解决项目中各个库之间的依赖关系。其核心机制依赖于一个称为 SAT 求解器（SAT Solver）的算法。这个求解器的作用是：在众多可能的包版本组合中，找出一组满足所有依赖约束的版本集合，或者判断无解。
什么是 SAT 问题？
SAT 是“可满足性问题”（Satisfiability Problem）的缩写，属于计算机科学中的经典逻辑问题。给定一组布尔变量和一系列逻辑表达式（如 (A 或 B) 且 (非 C 或 A)），SAT 求解器的任务是判断是否存在一组变量赋值，使得整个表达式为真。
Composer 将依赖解析问题转化为一个布尔逻辑问题，然后使用 SAT 求解器来寻找可行解。
如何将依赖关系转化为逻辑表达式？
Composer 把每个包的每个版本看作一个“原子命题”，然后用逻辑规则描述依赖、冲突和选择限制。例如：
- 依赖关系：如果项目 require "package-a:^2.0"，意味着必须选择 package-a 的 2.x 版本之一。这可以表示为：选择 package-a/2.0 或 package-a/2.1 或 ... 并且不能选择 1.x 或 3.x。
- 传递依赖：如果 package-a/2.1 依赖 package-b:^1.5，那么选择 package-a/2.1 就隐含了必须选择 package-b 的 1.5 或更高 1.x 版本。
- 冲突规则：某些包版本互不兼容，比如 package-b/2.0 与 package-c/
- 互斥选择：同一个包的不同版本是互斥的——只能选一个。这通过“至多选一个”这样的逻辑约束实现。
所有这些规则被翻译成合取范式（CNF, Conjunctive Normal Form），也就是“与”连接的多个“或”子句，这是大多数现代 SAT 求解器的标准输入格式。
Composer 使用的求解流程
Composer 并不是从头实现一个完整的 SAT 求解器，而是基于 picosat 这样的高效 C 实现，并通过 PHP 扩展调用。它的依赖解析流程大致如下：
- 读取所有已知包及其版本信息（来自本地缓存或远程仓库）。
- 遍历每个包版本，生成对应的依赖、冲突和替换规则。
- 将这些规则编译为布尔变量和 CNF 子句。
- 调用 SAT 求解器尝试找到一组变量赋值（即哪些包版本被选中）满足所有子句。
- 如果求解成功，输出具体的包版本列表；如果无解，报错并提示无法满足依赖。
在这个过程中，Composer 还会加入一些优化策略，比如版本范围的预处理、依赖扁平化、优先选择稳定版本等，以减少搜索空间和提升求解效率。
为什么使用 SAT 而不是简单的递归查找？
早期的依赖管理器常采用“贪心算法”或“深度优先搜索 + 回溯”的方式逐个安装依赖。但这类方法在面对复杂依赖时容易陷入局部冲突，难以发现全局最优解，甚至错过本可满足的解。
SAT 求解器的优势在于：
- 完整性：能系统性地探索所有可能性，确保不会遗漏可行解。
- 高效剪枝：现代 SAT 求解器使用冲突驱动子句学习（CDCL）等技术，能在发现矛盾时快速回溯并记录原因，避免重复搜索。
- 表达能力强：可以自然表达“或”、“非”、“互斥”等复杂逻辑，适合描述现实世界中复杂的依赖和冲突规则。
基本上就这些。Composer 借助 SAT 求解器，把看似混乱的依赖问题变成一个形式化的逻辑问题，从而高效、可靠地找到解决方案。这套机制也让 Composer 在处理大型项目或多层嵌套依赖时表现得更加稳健。
