Composer 的 Solver 是自研的回溯式约束引擎，基于 DFS 与 CDCL 风格冲突学习，处理版本区间而非原子变量，通过单元传播与冲突驱动剪枝压缩搜索空间；composer.lock 是已验证可行解，install 直接复用，update 则全局或局部重解。
Composer 的 Solver 不是传统 SAT 求解器，而是带剪枝的回溯式约束引擎
它不调用 MiniSat 或 Z3 这类通用 SAT 工具，也没有把整个问题转成标准 CNF 公式扔给外部求解器。实际用的是 Composer 自研的 Solver 类，核心是一个深度优先搜索（DFS）+ 冲突驱动学习（CDCL 风格）的约束满足引擎。
关键区别在于：它处理的是「版本区间」而非原子布尔变量。比如 "monolog/monolog": "^2.0" 不会拆成 monolog/monolog:2.0.0、monolog/monolog:2.0.1……上千个变量，而是先归约为区间 [2.0.0, 3.0.0)，再在解析过程中动态展开具体候选版本——这大幅压缩了搜索空间。
- 所有依赖、conflict、replace、provide 规则都被转为可执行的逻辑条件（如
if $A === 'v1.0' then $B must be in [2.0, 3.0)） - 每次选择一个包版本后，立即做「单元传播」：推导出必须启用/禁止的其他版本（例如某 PHP 版本不兼容，整批包直接被标记为不可选）
- 一旦发现矛盾（如两个包分别要求
php:^7.4和php:^8.1），就记录该冲突路径，并在后续搜索中跳过同类组合
为什么 composer update 有时卡住或报错，而 composer update foo/bar 却能成功？
因为全局求解是 NP-hard 问题，搜索空间随包数量指数增长；但局部更新只固定其余已解析结果，只重解与 foo/bar 直接相关的子图——相当于把大迷宫缩成一条走廊。
-
composer update：从根依赖开始，重新构建整个依赖图，尝试所有可能的版本组合路径 -
composer update foo/bar：复用composer.lock中其余包的版本，仅对foo/bar及其直系依赖做增量求解 - 若你手动改过
composer.json但没删composer.lock，Composer 仍会以 lock 文件为起点做“最小变更”，这常掩盖真实冲突
常见现象：composer update 卡在 “Resolving dependencies…” 超过 2 分钟，大概率是遇到了组合爆炸；此时可加 -v 查看最后尝试的包版本链，或改用 composer update --with-dependencies foo/bar 精准干预。
composer install 为什么快？composer.lock 到底存了什么？
composer.lock 不是日志，也不是缓存，它是上一次 Solver 成功输出的「已验证可行解」——精确到每个包的完整版本号、源类型（dist/source）、SHA256 校验和、安装路径及依赖映射。
-
composer install完全跳过求解过程，只按 lock 文件逐条下载 + 校验 + 解压，所以秒级完成 - 一旦你手动编辑
composer.lock（比如改了个哈希值），下次install会失败，因为校验不通过；而update会无视你的修改，重新生成一份 - lock 文件里还存了
platform信息（如"php": "8.1.22"），这是 Solver 当时运行环境的快照，影响版本筛选结果
{
"packages": [
{
"name": "monolog/monolog",
"version": "2.9.1",
"dist": {
"type": "zip",
"url": "https://api.github.com/repos/Seldaek/monolog/zipball/...",
"reference": "a1b7d5e...",
"shasum": "e8a9f3..."
}
}
],
"platform": {
"php": "8.1.22"
}
}
冲突报错里那条 “root requires X, but Y requires Z” 是怎么来的？
这不是完整依赖图，而是 Solver 在回溯失败后，从冲突点向上追溯找到的「最短不可满足子集」（MUS）。它刻意省略中间冗余节点，只保留对用户最有诊断价值的一条矛盾链。
- 例如你 require
"laravel/framework": "^10.0"，而某个 dev 包"nunomaduro/collision": "^7.0"要求"laravel/framework": "^9.0"，报错就聚焦在这对冲突，不会扯进symfony/console或phpunit/phpunit - 它不解释“为什么不能降级 Laravel”，因为 Solver 的目标不是协商，而是证明无解——这条路径已足够构成反证
- 若想看到更广的上下文，可用
composer depends --tree monolog/monolog手动查依赖树，或加--debug看 Solver 的决策日志
真正容易被忽略的是：Solver 的「确定性」。它每次运行在相同输入（composer.json + lock + platform）下，必然产生相同输出。所谓“随机冲突”往往源于本地环境差异（PHP 版本、扩展缺失、镜像源不同步）或 lock 文件未提交导致团队环境不一致。
