Composer使用SAT Solver解决PHP项目中的依赖冲突，它将包版本和依赖规则转化为布尔逻辑表达式，通过构建CNF公式并运用DPLL算法求解，确保所有依赖约束被满足，相比传统递归方法能更高效地找到可行解。
Composer 是 PHP 的依赖管理工具，它的核心功能之一是解决项目所需的库及其版本之间的依赖关系。当项目中引入多个第三方包时，这些包可能彼此依赖不同版本的同一个库，甚至存在冲突。为了解决这种复杂的依赖网络，Composer 使用了 SAT Solver（布尔可满足性求解器）来计算出一组能满足所有约束条件的依赖组合。
什么是 SAT Solver？
SAT Solver 全称是 "Boolean Satisfiability Solver"，即布尔可满足性求解器。它用于判断是否存在一组变量赋值，使得一个布尔逻辑表达式为真。在软件依赖解析场景中，这个“表达式”就是项目的依赖约束集合，而“变量”则是各个包的安装与否或具体版本选择。
Composer 将依赖问题转化为一个逻辑命题：是否存在一种方式安装某些包、不安装另一些包，并选择合适的版本，使得所有声明的依赖规则都被满足？这个问题被建模成一个 SAT 问题，然后由专门的算法去求解。
依赖关系如何转化为逻辑表达式
Composer 把每个可用的包版本视为一个原子命题。例如：
- A@1.0 表示安装包 A 的 1.0 版本
- not A@1.0 表示不安装该版本
接着，将依赖规则翻译成子句（clause），也就是逻辑“或”的组合。常见规则如下：
依赖声明（require）：如果 B@2.0 要求 A >= 1.0，则表示只要安装 B@2.0，就必须安装 A 的某个满足 >=1.0 的版本。这可以写成逻辑形式：
(not B@2.0) OR (A@1.0 OR A@1.1 OR A@2.0 ...)
冲突声明（conflict）：若 C@1.0 与 D@3.0 不兼容，则不能同时安装两者：
(not C@1.0) OR (not D@3.0)
互斥安装（同一包的不同版本）：不能同时安装 A@1.0 和 A@1.1：
(not A@1.0) OR (not A@1.1)
最终，Composer 构造出一个巨大的 CNF（合取范式）公式 —— 多个子句通过 AND 连接，每个子句是若干文字（literal）的 OR 组合。SAT Solver 的任务就是找出使整个公式为真的变量赋值方案。
Composer 中的实现机制
Composer 并非从头开发 SAT 求解器，而是基于 php-SAT 或类似的底层库（如 minisat 的思想移植），使用现代 DPLL（Davis-Putnam-Logemann-Loveland）算法变种进行搜索。
主要步骤包括：
- 构建包池（Pool）：收集所有可用的包版本信息，包括它们的依赖、冲突、替换和建议等元数据。
- 编码为布尔变量：为每一个可能被安装的包版本创建对应的布尔变量。
- 生成规则子句：根据 require、conflict、replace 等字段生成逻辑约束子句。
- 运行 SAT 求解：调用求解器尝试找到一组真值分配，使得所有子句成立。
- 回溯与优化：如果没有解，Composer 可能放宽约束（比如忽略某些次要依赖）；如果有多个解，会选择更稳定或更高版本的组合。
值得一提的是，Composer 在实际中还加入了启发式策略，比如优先选择最新稳定版本、尽量复用已锁定版本（来自 composer.lock）等，以提升解析效率和结果一致性。
为什么需要 SAT Solver？传统方法有什么不足
早期的包管理器多采用简单的递归合并策略：逐个处理依赖，遇到新包就加入，发生冲突则报错。这种方法在面对复杂依赖图时极易失败，即使存在可行解也无法发现。
举例来说：
- 你的项目 require 包 X 和 Y
- X requires A@1.0
- Y requires A@2.0
表面上看冲突了，但如果 A 提供了统一接口，且 X 和 Y 实际上都能接受 A@2.0（只是未声明），传统解析器会直接报错，而 SAT Solver 有能力探索更多可能性，识别出 A@2.0 是可接受的解。
SAT Solver 能全局看待问题，穷举并剪枝搜索空间，从而找到隐藏的可行路径，显著提高解析成功率。
基本上就这些。Composer 借助 SAT Solver 实现了强大、可靠的依赖解析能力，让用户不必手动协调版本冲突，背后是一整套严谨的逻辑建模与高效算法支撑。
