Composer使用自研回溯式约束满足算法而非传统SAT求解器，核心是带剪枝的DFS回溯引擎，将依赖约束转为版本区间与逻辑条件，目标是找到满足所有require约束的版本组合并清晰解释冲突。
Composer 的依赖解析器在遇到冲突时，并不使用传统意义上的 SAT 求解器（如 MiniSat、Z3），而是基于一个**自研的回溯式约束满足算法**，核心目标是找出一组满足所有 require 约束的包版本组合；当无解时，它会尝试推导出最清晰、最具解释性的冲突原因，而非随机失败。
它不是真正的 SAT Solver，但借鉴了约束传播思想
早期文档中提到“SAT solver”是一种类比说法，强调其目标是求解布尔可满足性问题（即：是否存在一组版本分配，使所有依赖规则同时为真）。实际上，Composer 使用的是：
- 一个带剪枝的深度优先搜索（DFS）回溯引擎
- 依赖约束被转化为“版本区间”和“逻辑条件”（如
^2.0→>=2.0.0 ） - 在安装/更新过程中动态构建“包-版本”选择图，边表示兼容性或冲突
- 通过“冲突驱动学习”（Conflict-Driven Clause Learning, CDCL）的简化思想识别不可行分支并跳过——比如发现
packageA:1.0和packageB:2.0共同要求php:^7.4与php:^8.1，则直接标记该组合无效
冲突发生时，它如何决策“谁该让步”？
Composer 不会主观决定哪个包“更重要”，而是按确定性策略探索解空间。它的决策依据是：
-
安装顺序优先级：根
composer.json中直接声明的依赖（require）拥有最高固定性；它们的版本范围不会被随意降级或跳过 -
版本范围宽度优先收缩：在回溯中，优先尝试收紧更宽泛的约束（例如把
*或^1.0缩小到具体小版本），而非强行升级一个已锁定的包 -
最小变更原则：如果已有
vendor/目录，Composer 会尽量复用已安装版本，仅调整引发冲突的少数几个包——这也是为什么composer update foo/bar比composer update更容易成功 - 冲突溯源路径最短化：报错信息里显示的“root requires X, but Y requires Z”链路，是它找到的最短逻辑矛盾路径，不是全部依赖图
你看到的 “Your requirements could not be resolved” 是怎么来的？
当 DFS 走完所有可行分支仍无解，Composer 就终止搜索并生成冲突报告。这个过程包括：
- 记录最后一次成功推进的“决策点”（比如选了
monolog:2.8.0） - 回溯到最近一个有多个选项的节点，尝试下一个候选版本
- 若所有候选都触发新冲突，则向上合并冲突原因，直到能归结到根依赖或 PHP 版本等硬约束
- 最终输出的冲突树，是它认为对用户最有诊断价值的一条矛盾链，而非穷举所有可能冲突
基本上就这些。它不复杂，但容易忽略的是：Composer 的“决策”本质是系统性排除 + 确定性回溯，不是 AI 推理，也不做权衡取舍——没解就是没解，报错里的那条路径，已经是它能找到的最简反证。
