Composer使用SAT求解器将依赖管理转化为布尔可满足性问题，通过将包版本视为布尔变量、依赖规则转化为逻辑表达式，利用回溯与启发式搜索寻找满足所有约束的安装方案，相比递归方法能全局分析冲突、精确处理复杂依赖，并可证明无解情况，提升解析准确性与可靠性。
Composer 的依赖解析器使用一种基于 SAT（Boolean Satisfiability Problem，布尔可满足性问题）求解的技术来解决 PHP 项目中复杂的依赖关系。它的核心目标是：在众多包及其版本约束之间，找出一组能满足所有依赖规则的版本组合，或者判断这样的组合不存在。
什么是 SAT 求解器？
SAT 求解器原本是计算机科学中的一个理论工具，用于判断一组布尔变量能否被赋值，使得整个逻辑表达式为“真”。Composer 将这个思想应用到依赖管理中：把每个“包的安装与否”看作一个布尔命题，把依赖、冲突、版本约束等转化为逻辑规则，然后让求解器找出一个“可满足”的安装方案。
如何将依赖转换为逻辑表达式？
Composer 把每一个包的每一个版本都视为一个独立的命题。比如：
- foo/bar v1.0 存在或不存在（true 或 false）
- foo/bar v2.0 同样是一个布尔变量
然后根据 composer.json 中的 require 和 conflict 规则，生成逻辑子句。例如：
- 项目 require foo/bar ^1.0 → 必须选择 v1.0 或 v1.5，但不能选 v2.0
- bar/baz v3.0 requires foo/bar ^1.0 → 如果选择了 bar/baz v3.0，则必须满足 foo/bar 是 1.x 版本
- qux/quux v1.2 conflicts with foo/bar
这些规则会被翻译成类似“ (bar/baz@v3.0 → foo/bar@v1.0 ∨ foo/bar@v1.5) ”这样的逻辑蕴含式，最终形成一个巨大的布尔公式。
求解过程：搜索与回溯
Composer 的 SAT 求解器会尝试为每个包版本变量赋值（安装或不安装），逐步构建一个可行解：
- 从根包的需求开始，逐个引入依赖
- 每当添加一个包时，检查其依赖是否能被满足
- 如果某个选择导致矛盾（如两个包互相冲突），就回溯，尝试其他版本
- 使用启发式策略优先选择更稳定或更常见的版本，加快收敛速度
这个过程类似于走迷宫：每一步选择一个包版本，沿着路径走下去，遇到死胡同就退回上一步换路。最终找到一条通路（即所有依赖都被满足），或确认无解。
为什么用 SAT 而不用简单递归？
传统的递归依赖解析容易陷入局部最优或无法处理复杂冲突。而 SAT 方法的优势在于：
- 能全局看待所有约束，避免遗漏隐式冲突
- 支持精确的版本排除和替代（provides/replaces）
- 可以证明“无解”，而不是无限尝试
- 经过优化后，在大多数实际场景中性能可接受
基本上就这些。Composer 借助 SAT 求解器把依赖管理变成一个形式化推理问题，虽然计算复杂度高，但在实践中通过剪枝和缓存大大提升了效率。理解这一点有助于我们写出更清晰的版本约束，减少 lock 文件冲突和安装失败。
