Composer不使用SAT求解器，而是采用自研的回溯式依赖解析器，基于版本约束剪枝与深度优先尝试，将依赖规则映射为Package→[VersionConstraint]结构，而非CNF公式，其核心为BacktrackingSolver类中的tryToSolve()与backtrack()逻辑。
Composer 不用 SAT 求解器，它用的是自研的回溯式依赖解析器，不是基于布尔可满足性（SAT）问题建模的算法。
Composer 的 resolver 实际上是回溯 + 版本约束剪枝
Composer 的 Pool 和 RuleSet 构建过程会把所有包版本、require、conflict、provide、replaces 转成一组逻辑规则，但不转成 CNF 公式；它的 BacktrackingSolver 采用深度优先尝试 + 冲突驱动回退，类似 CSP（约束满足问题）求解器，但没有引入 SAT 求解器如 MiniSat 或 Z3。
- 每次选择一个未解决的 package，按版本稳定性（stable → RC → beta → alpha → dev）和语义化版本兼容性排序尝试
- 遇到冲突（例如
foo/bar ^2.0和foo/bar 1.9.0同时被 require）就回退并换另一个版本 - 通过
Pool::whatProvides()和RuleSet::getRulesForPackage()实现快速剪枝，避免穷举
为什么不是 SAT？常见误解来源
很多人看到“依赖冲突”“满足所有约束”就联想到 SAT，但 Composer 的约束本质是：版本范围交集是否为空、是否违反 conflict、是否满足 minimum-stability 等——这些是区间运算与显式排除，不是命题逻辑变量赋值问题。
- SAT 求解器需要把每个可能的包版本映射为一个布尔变量（如
phpunit-9.5.0 = true），再把所有约束转为子句，Composer 从没这样做 - Composer 的
Rule是Package -> [VersionConstraint]映射，不是 CNF 子句；ConflictRule直接触发回退，不参与合取范式构造 - 官方文档和源码注释中从未提及 SAT、DPLL、unit propagation 等术语；核心 resolver 类是
Composer\Installer\InstallationManager和Composer\DependencyResolver下的Pool/RuleSet/BacktrackingSolver
想验证？看实际 resolver 日志和源码路径
开启详细日志就能看到回溯行为，而不是 SAT 求解步骤：
composer install -vvv
关键源码位置：
-
src/Composer/DependencyResolver/Pool.php：构建所有可用包版本视图 -
src/Composer/DependencyResolver/RuleSet.php：存储所有规则（require/conflict/replace），不转 CNF -
src/Composer/DependencyResolver/BacktrackingSolver.php：主循环含tryToSolve()和backtrack()，无 SAT 接口调用
如果你在某篇文章里看到 “Composer uses a SAT solver”，那基本是作者混淆了 dependency resolution 的广义概念和具体实现机制——就像说“Git 用图论算法”，没错，但 Git 的拓扑排序不是调用 NetworkX。
真要用 SAT 解依赖？有替代方案但不实用
学术上确实有人把 PHP 包依赖建模为 SAT 问题（如早期的 packagist-sat PoC），但实际不可行：
- Packagist 上超 30 万个包，每个包平均 10+ 版本 → 布尔变量轻松破百万，CNF 子句爆炸
- PHP 的
conflict、provide、平台约束（如ext-curl）、platform-check难以干净映射到命题逻辑 - Composer 需要支持部分安装、
--with-all-dependencies、replace动态重写等运行时策略，SAT 模型难以增量更新
所以别在 composer.json 里期待 "solver": "z3" 这种配置项——它根本不存在，也不会存在。
