composer 用 SAT 求解依赖冲突而非贪心或回溯，因其能处理环状约束与多层间接冲突，如 A≥1.2、B∈[1.0,1.3]、C 同时依赖 A 和 B 且对 A 有额外要求。
Composer 的依赖解析不是简单的“找最新版”，而是把整个依赖图转化成一个布尔可满足性（SAT）问题，交给专门的求解器来判断是否存在一组版本组合，能让所有约束同时成立。理解这点，是调试棘手冲突的关键。
为什么用 SAT 而不是贪心或回溯？
php 项目依赖常出现“环状约束”和“多层间接冲突”，比如 A 要 v1.2+，B 要 v1.0–1.3，C 同时依赖 A 和 B，而 C 自身又要求 A
Composer 内部使用 clue/sat-solver 库，把每个包版本抽象为一个布尔变量（如 monolog/monolog:2.9.0 = true），把 require、conflict、platform 等规则翻译成子句（clause），例如：
-
"monolog/monolog": "^2.8"→ 至少选一个 2.8.x 版本 -
"php": ">=8.1"→ 排除所有 php "conflict": {"symfony/console": " → 若选了 symfony/console:6.1，则整个解无效
看懂 composer update 的冲突报告
当报错类似 Your requirements could not be resolved to an installable set of packages.，别急着删 vendor。先加 -v 或 --debug 运行：
-
composer update -v：显示每一步尝试的候选版本、为何被拒绝（如 “skipped: constraint … does not allow …”） -
composer update --debug：输出更底层的 SAT 变量名和子句冲突点，比如 “clause #1274 rejected because …”
重点看最后一段 “Problem 1”，它通常指出第一个无法调和的约束链。不是最上面那个包的问题，而是它触发了底层逻辑矛盾。
手动缩小搜索空间（实用技巧）
SAT 求解时间随变量数指数增长。你不需要读懂所有子句，但可以帮 Composer 减负：
- 临时注释掉非核心 dev 依赖（如 phpunit、infection），运行
composer update --no-dev看是否能解——排除测试工具引发的间接冲突 - 用
composer prohibits vendor/package查谁在阻止某个版本，比翻 require 树快得多 - 对可疑包，显式指定宽松约束，比如改
"foo/bar": "1.2.3"为"foo/bar": "^1.2"，给求解器更多自由度 - 检查
platform配置是否过于严格（如"php": "8.2.0"锁死小版本），建议写成"php": "^8.2"
进阶：用 composer show + dot 输出依赖图
有时冲突来自深层传递依赖。生成可视化图有助于发现隐藏路径：
-
composer show -t：树状列出当前已装依赖及来源 -
composer show --tree monolog/monolog：查谁拉入了 monolog 及其版本依据 - 配合
composer global require baethon/composer-graph，再运行composer graph --format=dot | dot -Tpng -o deps.png，导出图片看环与分叉
图中若出现同一包多个版本并存（如 laravel/framework v9.52 和 v10.48 同时被不同分支 require），基本就是 SAT 无解的根源。
基本上就这些。Composer 的 SAT 解析不神秘，它只是把你的 composer.json 当作逻辑命题来验证。越早学会读 debug 输出、缩小变量范围、查传递路径，就越少陷入“删了重装就好”的循环。