Composer 依赖解析采用 SAT 求解器进行全局逻辑验证，将版本选择建模为布尔变量与约束子句，通过单元传播和冲突分析高效求解可行解，并以 composer.lock 快照保存结果。
Composer 的依赖解析不是靠“试错”或“贪心匹配”，而是把整个版本选择问题转化成一个逻辑判断题——用 SAT（Boolean Satisfiability，布尔可满足性）求解器来求解。
把包版本变成真假变量
每个可能的包版本（比如 monolog/monolog:2.8.0、monolog/monolog:2.9.1、symfony/console:6.4.3）都被建模为一个布尔变量：选它就是 true，不选就是 false。Composer 不会穷举所有组合，而是用约束规则压缩搜索空间。
- 一个包在同一时间只能有一个版本被启用（互斥约束）
- 如果选了 laravel/framework:^10.0，它要求 symfony/console:^6.2，那就必须同时满足这个子依赖（蕴含约束）
- 如果两个包分别要求 guzzlehttp/guzzle:^7.0 和 ^8.0，它们没有交集，SAT 就会判定“无解”并报 conflict
依赖规则翻译成逻辑子句
composer.json 里写的 ^2.0、~3.5.1、!=4.2.0 等，都会被转成 CNF（合取范式）形式的逻辑子句。例如：
- "monolog/monolog": "^2.0" → 允许 2.0.0 到 2.999.x，但排除 3.0.0+ → 对应一组“或”条件的组合子句
- "php": ">=8.1" → 所有不满足 PHP 版本的包版本变量直接设为 false
- conflict 字段 → 显式添加禁止同时为 true 的变量对
求解器快速收敛到可行解
Composer 内置的 SAT 求解器（如 Minisat 或自研轻量实现）并不暴力遍历，而是利用单元传播（unit propagation）、冲突分析（conflict-driven learning）等技术剪枝。它边推理边学习“哪些组合一定不行”，跳过大量无效分支。
- 目标不是找“所有解”，而是找一个满足全部约束的最小化、稳定、较新的版本组合
- 当存在多个可行解时，Composer 倾向选择语义化版本中“更靠右”的版本（即尽量用更新的小版本），兼顾兼容性与新鲜度
- 失败时返回的 conflict 信息，其实是求解器在回溯过程中发现的最小不可满足子集（MUS），也就是最精简的冲突根源
锁文件是求解结果的快照
composer.lock 不是日志，而是 SAT 求解器输出的“已验证可行解”。它记录了当前所有包的确切版本、哈希、源地址。下次 composer install 直接复用这个答案，跳过求解过程——所以快且确定。
- 改 composer.json 后运行 composer update，才会重新触发 SAT 求解
- 手动改 lock 文件 = 替换掉已验证解，很可能导致下次 install 失败或行为异常
基本上就这些。不复杂但容易忽略：它不是“挑最新版”，也不是“按顺序安装”，而是一次全局逻辑验证。
