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)
这种结构能被成熟的 SAT 求解器高效处理。求解器的任务就是找出一组 true/false 赋值，让整个公式为真——对应到实际，就是一套可行的包版本组合。
求解过程兼顾效率与可解释性
现代 Composer 使用增强型 SAT 求解器，不是暴力穷举，而是结合：
- 冲突驱动的回溯（CDCL）快速剪掉无效分支
- 版本优先级启发式（如倾向较新但兼容的版本）
- 缓存已验证的子问题结果，避免重复计算
- 一旦无解，能反向追踪出最小冲突集，生成类似“package-a v1.2 需要 laravel/framework ^10.0，但 package-b v3.4 要求 ^9.0”的精准报错
