Composer update卡在“Resolving dependencies…”时，SAT求解器正执行DFS+CDCL回溯搜索，通过单元传播验证版本组合是否满足全部约束。
Composer 的依赖解析器不是“试错式安装”，而是基于约束满足的逻辑推理过程；它不靠运气找版本，而是用 SAT 风格的回溯引擎证明是否存在一组版本组合能同时满足所有规则。
composer update 卡在 “Resolving dependencies…” 是什么在运行？
此时 Solver 正在执行 DFS + CDCL 风格的搜索：从根依赖出发，逐个为包选择候选版本，每选一个就立即做单元传播（例如：选了 php:^8.1，则所有声明 "conflict": {"php": " 的包瞬间被排除）。
- 传播失败（比如某包无可用版本满足当前约束）会触发回溯，撤销上一步决策
- 冲突路径会被记录并用于剪枝，避免重复进入已证伪的分支
- 搜索空间实际是「版本区间」而非全部原子版本，例如
^2.0被抽象为[2.0.0, 3.0.0)，具体候选只在必要时展开 - 若未加
-v，你完全看不到中间状态；加了后能看到最后尝试的包链，比如monolog/monolog:2.10.0 → symfony/polyfill-php81:1.29.0 → php:8.1.22
为什么 composer install 很快，而 composer update 经常失败？
install 直接读取 composer.lock 中已验证的解，跳过求解；update 则重跑整个求解流程，且默认是全局重解——哪怕只改了一个 require，也会把整个依赖图当作新问题处理。
-
composer.lock不是缓存，而是 SAT 求解器输出的「可行解快照」，包含每个包的确切版本、哈希、来源和嵌套依赖关系 - 手动修改
composer.json后不删composer.lock，Composer 仍以 lock 文件为起点做最小变更，这可能掩盖真实冲突（比如旧 lock 强制保留某个已被新版 require 排除的包） - 局部更新（如
composer update monolog/monolog）会复用 lock 中其余包的版本，只重解该包及其直系依赖子图，大幅降低复杂度
版本约束如何影响求解难度？
约束越宽泛，候选版本越多，搜索空间越大；但约束太窄（如写死 "1.2.3"）反而容易因上游包升级导致间接冲突无法传播化解。
-
^1.2.3和~1.2.3表达的是不同区间：^允许主版本内任意兼容升级（[1.2.3, 2.0.0)），~只允许补丁级升级（[1.2.3, 1.3.0)），后者更易满足但灵活性差 - 混用
^和~在大型项目中会加剧区间交集计算负担，Solver 需反复收缩各包的可选版本范围 - PHP 版本约束（如
"php": "^8.0"）是全局锚点，一旦与某个包的conflict或require冲突，整个分支立刻失效
真正难的不是“找不到版本”，而是“找不到一组互不矛盾的版本”；Solver 的输出（成功或报错）本质是对约束系统一致性的一次形式化验证——这点常被忽略，但决定了你是否该先检查 composer.lock 是否过期，还是直接换策略局部更新。
