SAT求解是判断布尔公式能否为真的过程，Composer将其用于依赖解析，通过将版本约束转化为逻辑表达式，利用SAT求解器确定是否存在满足所有依赖条件的包版本组合。
Composer 的依赖解析器使用了一种基于 SAT 求解器（布尔可满足性求解）的技术来解决复杂的依赖关系问题。它的核心目标是：在给定一组包及其版本约束的前提下，找出一组能满足所有依赖条件的包版本组合，或者确定这样的组合不存在。
什么是 SAT 求解？
SAT（Satisfiability）问题是计算机科学中的一个经典逻辑问题：判断是否存在一组布尔变量的赋值，使得一个布尔公式为真。Composer 将依赖管理问题转化为一个逻辑表达式，然后用 SAT 求解器来判断这个表达式是否“可满足”——也就是是否存在一个可行的安装方案。
例如，你项目中 require 了 A 和 B 两个包：
- A 需要 php >= 7.4 且依赖 C ^2.0
- B 需要 C ^1.5
这些条件会被翻译成类似“C 必须同时满足 ≥1.5 且
Composer 如何建模依赖问题？
Composer 把每个包的每个版本看作一个“原子命题”。比如：
- C-1.5.0 表示“安装 C 的 1.5.0 版本”
- C-2.0.0 表示另一个独立命题
然后通过逻辑规则连接这些命题：
- 互斥性：不能同时安装 C-1.5.0 和 C-2.0.0（同一包的不同版本互斥）
- 依赖关系：A-1.0.0 → C-^2.0（如果安装 A-1.0.0，则必须安装符合 ^2.0 的 C 版本）
- 版本约束：^2.0 转换为具体版本范围，如 ≥2.0 且
整个依赖图被编译成一个巨大的布尔公式，SAT 求解器尝试为每个包版本变量分配“安装”或“不安装”，使得整体公式为真。
实际解析过程的关键优化
直接暴力搜索所有组合不可行（组合爆炸）。Composer 使用了多种优化策略：
- 单位传播：如果某个条件强制选择了某个版本（如只有 C-2.0 满足某依赖），就立即确定它，并推导出其他相关约束
- 回溯搜索：尝试假设某个版本可用，一路推导；遇到矛盾就回退，换另一个可能
- 冲突驱动学习：记录导致失败的原因（如“A-1.0 和 B-3.0 冲突”），避免重复探索相同错误路径
- 版本归约：对语义化版本进行区间合并，减少需要考虑的具体版本数量
为什么有时解析很慢或失败？
尽管有优化，复杂项目仍可能出现：
- 大量包和版本导致搜索空间巨大
- 多个间接依赖提出互相矛盾的版本要求
- 平台约束（PHP 版本、扩展等）进一步限制选择
当 Composer 报错“无法解析依赖”时，通常意味着 SAT 求解器遍历了所有可能路径后确认无解。你可以通过简化 require、锁定某些版本或调整平台配置来帮助求解器更快找到答案。
基本上就这些。Composer 的 SAT 解析器把现实世界的依赖问题变成了一个逻辑推理任务，虽然底层复杂，但对用户来说，它默默工作，只在必要时报错。理解其原理有助于更理性地处理依赖冲突。
