SAT求解是判断布尔公式可满足性的逻辑问题，Composer将其用于依赖解析：将包版本视为布尔变量，依赖冲突等规则转为逻辑子句，最终求解一组版本组合使所有条件成立。
Composer 使用一种基于 SAT（可满足性问题）求解的算法来解析项目依赖关系。它的核心目标是：在众多包版本及其复杂的依赖约束中，找出一组能满足所有依赖条件的版本组合，或者判定无解。
什么是 SAT 求解？
SAT（Satisfiability）问题是逻辑学中的经典问题，判断是否存在一组变量赋值，使得一个布尔公式为真。Composer 将“依赖解析”转化为一个逻辑表达式问题：
- 每个“包版本”被视为一个布尔变量（是否被安装）
- 依赖、冲突、推荐等规则转换为逻辑子句（如 A 要求 B，表示为 A → B）
- 最终目标是找到一组“安装哪些版本”的真值分配，使所有子句都成立
Composer 如何构建逻辑表达式？
Composer 在解析过程中将依赖关系翻译成逻辑规则：
- 依赖（require）：如果安装包 A 的 1.0 版本，就必须安装 B 的 ^2.0 版本。这会生成形如 “A:1.0 → (B:2.0 ∨ B:2.1 ∨ B:2.2)” 的子句
- 冲突（conflict）：A:1.0 与 C:
- 互斥（replace/provide）：某些包功能相同，只能装一个，生成排他性子句
- 根包要求：用户 composer.json 中的要求作为必须满足的前提条件
求解过程简述
Composer 借助一个名为 phpsat 的内部 SAT 求解器变种，采用类似 DPLL 算法的回溯搜索策略：
- 从根包开始，逐步尝试选择包版本
- 每做一次选择，立即检查是否违反已有规则（传播约束）
- 若出现矛盾（如某个包既必须安装又被排除），则回溯并尝试其他版本
- 通过启发式方法优先尝试更可能成功的路径（例如选择依赖较少的版本）
- 直到所有包都被确定版本且无冲突，或确认无解为止
为什么用 SAT 而不是简单递归？
传统的递归下降解析在面对复杂依赖时容易陷入局部最优或无法发现深层冲突。SAT 求解的优势在于：
- 能全局看待所有约束，避免“先入为主”的错误决策
- 支持精确的冲突分析，失败时可提供较清晰的原因
- 理论上能穷尽所有可能性，确保结果是最优或确实无解
基本上就这些。Composer 的 SAT 解析器虽然复杂，但正是它保证了你在运行 composer install 时，能得到一个一致且可工作的依赖树。
