Composer的依赖解析算法（SAT Solver）是如何工作的？（原理解析）

Composer将每个包版本建模为布尔变量（如monolog/monolog:2.9.0为true表示被选中），同一包版本互斥；require、依赖和conflict规则均转译为逻辑表达式，如require "symfony/console": "^6.0" 表示必须选中6.0.x中至少一个版本且不可选5.x或7.x。

把每个包版本变成“是或否”的命题

Composer 不把依赖当成简单的“下载列表”，而是建模成逻辑判断问题。它为每个包的每个可用版本创建一个布尔变量，比如 monolog/monolog:2.9.0 表示“这个版本被选中”，值为 true 或 false。同一包的不同版本互斥——不能同时为 true，这通过逻辑子句强制约束。

把依赖规则翻译成逻辑条件

所有你在 composer.json 里写的声明，都会被转译为逻辑表达式：

• require "symfony/console": "^6.0" → 翻译为：必须选中 6.0.x 中的至少一个版本（如 6.0.0、6.1.2），不能选 5.x 或 7.x
• A 依赖 B ^2.0 → 写成蕴含式：如果 A 被选中，则 B 的某个 ≥2.0 且
• conflict "php": " → 直接禁止 php 版本低于 8.1 的所有组合成立
• replace "old/package" → 加入“选 new/package 就不能选 old/package”的排斥子句

用合取范式（CNF）统一表达所有约束

Composer 把全部命题和规则整理成标准形式：多个“或子句”的“与”组合，即 CNF（Conjunctive Normal Form）。例如：

(A∨B) ∧ (¬A∨C) ∧ (¬B∨¬C)

标签： php js json composer