依赖关系解析是程序员通常认为理所当然的事情。无论是它 cargo ， npm 还是您使用的任何包管理器，当这个黑匣子自己找出应该安装的特定软件包集时，没有人会感到惊讶。

不过，对我来说，这是一项令人着迷的壮举。当一台机器解决这样的抽象问题时，感觉很神奇，而我作为用户的输入最少！因此，当 Prefix.dev 的好人聘请我为 Conda 包生态系统创建一个开源依赖项求解器时，我很高兴。并不是说我是该主题的专家（远非如此！），但我确实知道我的 Rust 并且我是一个快速学习者。事实上，5周后，新的求解器终于可以作为响尾蛇 1 项目中的实验选项使用！

功劳归功劳，我能够在 Prefix 对响尾蛇的出色工作以及对 @wolfv 的不懈测试的基础上再接再厉，他一次又一次地设法打破了我的求解器......直到它终于奏效！

现在，如果你有兴趣，你可以跟着我进入依赖解析兔子洞。那里有很多有趣的东西可以看！

1. 背景

如果您想直接转到 SAT 求解器的内容，请随时跳过本节。

响尾蛇不是已经有了依赖关系解决器吗？

是的，它是libsolv的一个分支，但事实证明维护和扩展具有挑战性，因为它是用非常低级的C编写的。

所以你“用 Rust 重写了它”？

是的，感谢 NumFOCUS 的慷慨资助。我们调用了生成的库 libsolv_rs ，因为它主要是libsolv C库的一个端口，尽管它目前只支持解决Conda包。

依赖关系解析是什么意思？

您可能已经看到过 Cargo.toml 类似文件的东西，如下所示（大多数包管理器都有自己的自定义配置格式，但想法是相同的）：

[package]

name = "foo"
version = "0.1.0"
edition = "2021"

[dependencies]
rand = "*"

在这里，我们指定我们的项目需要 rand 软件包（crate，用 Rust 的说法），并且我们对任何版本都感兴趣。当我运行 cargo build 这个项目时，cargo 将 rand 依赖关系解析为最高可用版本，在撰写本文时为 0.8.5 .它还将为 的依赖项、它们的依赖项等找到 rand 合适的版本（然后，已解析依赖项的整个列表将存储在 中 Cargo.lock ）。

从依赖需求（例如安装任何 rand 版本的）到具体的软件包树（例如安装 rand 版本 0.8.5 ，及其对 x 版本的 0.2 依赖关系等）的过程称为依赖解析。在这个例子中，它可能看起来微不足道，但肯定不是！（如果你不相信我，请继续😉阅读）

2. 新的依赖关系求解器

我们已经提到了“求解器”这个词，但我们的意思是什么？在一般意义上，我会说求解器是一个程序，它接收数学问题作为输入，并将解决方案作为输出返回。这使它成为一个求解器，对吧？它的生活目标是解决。

在依赖关系解析的世界中，求解器是基于一些顶级依赖关系规范构造具体依赖关系树的引擎。在许多情况下，像我们一样，在幕后使用实际的 SAT 求解器（更多内容见下文）。这使得名称解析器更加合适！

从必需的依赖项到 SAT

让我们从一个例子开始。我有一个名为 的包，它 foo 0.0.1 取决于 bar （任何版本都可以）。为了能够运行我的包，我需要安装的版本 bar ，包括其传递依赖项。然后，求解器应该告诉我要安装的 bar 确切版本及其依赖项。下面是“依赖关系解决问题”的非正式定义：

  • 我的软件包 foo 0.0.1 依赖于任何 bar 版本的

  • 包存储库中 bar 有两个可用的版本：

    • bar 0.1.0 ，这取决于 baz 0.1.0
    • bar 0.2.0 ，这取决于 baz 0.2.0

  • baz 0.2.0 最近已从包存储库中删除

  • 我想知道应该安装哪些具体的软件包，以便 foo 的依赖项可用

上面的描述对于计算机来说太非正式了，但我们可以将其转换为布尔满足性问题（通常缩写为 SAT）。为此，您需要创建一个表示问题的布尔子句列表（其想法是每个子句的计算结果应为 true）。下面是从上述描述派生 2 的子句列表，其中每个变量对应于可以安装的包：

  1. (foo 0.0.1) ：必须始终安装根包 foo 0.0.1
  2. (foo 0.0.1 => bar 0.1.0 ∨ bar 0.2.0) ：如果已安装，则必须 foo 0.0.1 至少安装一个用于其 bar 依赖项的软件包
  3. (bar 0.1.0 => baz 0.1.0) ：如果已安装，则 bar 0.1.0 baz 0.1.0 也必须安装
  4. (bar 0.2.0 => baz 0.2.0) ：如果已安装，则 bar 0.2.0 baz 0.2.0 也必须安装
  5. (¬bar 0.1.0 ∨ ¬bar 0.2.0) ：您最多可以 bar 安装一个版本的
  6. (¬baz 0.1.0 ∨ ¬baz 0.2.0) ：您最多可以 baz 安装一个版本的
  7. (¬baz 0.2.0) ：您无法安装 baz 0.2.0 ，因为它不在软件包存储库中

求解器应该如何处理子句？它必须找到每个变量的值（真或假），使每个子句（从 1 到 7）的计算结果为 true。求解器完成后，依赖关系树由已设置为 true 的所有变量组成。让我们计算出前面的条款，看看它的实际效果：

  • true 分配给 foo 0.1.0 ，每个子句 1（没有其他方法可以使子句 1 的计算结果为 true）
  • 根据 baz 0.2.0 子句 7 分配给 false （没有其他方法可以使子句 7 的计算结果为 true）
  • 根据 bar 0.2.0 子句 4 赋值给 （鉴于前面的变量赋值 false ，没有其他方法可以使子句 4 的计算结果为 true）
  • 根据 bar 0.1.0 子句 2 赋值 （鉴于前面的变量赋值 true ，没有其他方法可以使子句 2 的计算结果为 true）
  • 根据 baz 0.1.0 子句 3 赋值 （鉴于前面的变量赋值 true ，没有其他方法可以使子句 3 的计算结果为 true）
  • 完成，因为所有子句的计算结果都为 true

那么依赖关系树中包含哪些包呢？那些被设置为true： foo 0.1.0 -> bar 0.1.0 -> baz 0.1.0 。

SAT解决

由于我们能够在布尔子句（如上面列出的子句）中表达依赖解析问题，因此我们可以将它们 3 提供给 SAT 求解算法以获得解决方案。

但是，上面的示例并不代表解决实际依赖关系问题所涉及的复杂性。到目前为止，我们只研究了当子句“强迫”我们这样做时为变量赋值的过程（即赋值是必需的，因为否则子句的计算结果为 false）。这也称为单位传播，是 SAT 求解器中使用的核心算法之一（有效地实现它需要一些聪明的技巧，例如观看文字，如果您阅读 MiniSAT 论文，您会发现）。

但是，单元传播不足以推动SAT求解过程完成。大多数实际方案都允许多种解决方案，因此通常没有设置变量值的“逻辑必要性”。你可以把它比作解决数独：有时你知道，一个数字必然应该进入一个特定的单元格。其他时候你必须猜测并希望你的猜测是正确的（你可能会发现你的猜测实际上是错误的，因为它导致了未来的不一致，在这种情况下你需要回溯）。

考虑到这一点，以下是我们使用的真实算法：

  1. 初始单元传播。总是至少有几个值可以在开始时传播，例如应该安装根包的事实（即它的变量应该设置为 true）。如果传播在此阶段遇到冲突的分配 4 ，这意味着原始需求无法满足（例如，用户想要安装不存在或彼此不兼容的软件包）。

  2. 求解器循环：

    1. 停止条件：如果所有子句的计算结果都为 true，我们就完成了。
    2. 设置：任意为尚未赋值的变量赋值。
    3. 传播：执行单元传播。如果传播完成且没有冲突，请返回到 1。
    4. 学习和回溯：找到导致冲突的作业组合并从中学习，这样我们以后就不会重复它们。如果冲突不可恢复，则意味着原始问题无法解决。如果可恢复，请回溯并返回到求解器循环的步骤 1。

同样，Rust 代码有很好的文档记录，并利用了可以指导您完成它的抽象，所以如果您想确切地了解底层工作原理，请不要犹豫。

有关学习的更多细节

对于求解者来说，从它看到的冲突中“学习”意味着什么？它如何能够找到冲突的原因？对于这篇已经很长的文章来说，这些问题的答案太长了，但如果你决心找出答案，这里有一些提示：我们使用的 SAT 求解算法称为冲突驱动条款学习 （CDCL）。MiniSAT论文提供了很好的介绍，甚至还有关于学习和回溯主题的幻灯片。

性能如何？

我们还没有进行基准测试，也没有努力优化任何东西。早期采用者报告说，解析器比libsolv慢，尽管仍然可以接受接近。一旦我们有了基准并开始迭代性能，我们希望更接近！

同样重要的是要注意，SAT 求解器的性能不是由低级技巧主导的，而是由所使用的算法主导的。SAT求解器已经在计算机科学领域研究了几十年，CDCL已经将自己确立为一种有效的算法，即使原始问题是NP完全的（它在几毫秒或几秒钟内找到解决方案，至少在依赖关系解决的特定领域）。我们真的站在巨人的肩膀上。

3. 尾声：在火车和求解器上

回到我在引言中提到的魅力，我不能不引用切斯特顿的“星期四的人”来结束这篇文章。在本书的这一片段中，诗人加布里埃尔·赛姆（Gabriel Syme）发表了关于火车奇迹的赞美演讲，你也可以将其应用于一般的计算机！

罕见的、奇怪的事情是达到目标;最恶心的，显而易见的事情是错过它。当人用一支狂箭击中远处的鸟时，我们觉得这是史诗般的。当一个狂野的引擎的人袭击一个遥远的车站时，这不是也是史诗般的吗？混沌是沉闷的;因为在混乱中，火车确实可以去任何地方，去贝克街或巴格达。但人是魔术师，他的全部魔力就在这里，他确实说维多利亚，瞧！是维多利亚。

这是我对报价的替代结束：

但是程序员是一个魔术师，他的全部魔力就在于此，他确实说“给我依赖树 x y ， z ”，瞧！它是y 、 z 、 的 x 依赖树。

  1. 您可以在包管理器的诞生中阅读有关 rattler 的更多信息。↩︎
  2. 如果您想了解如何将依赖关系 libsolv_rs 转换为布尔子句，请查看此处。该代码:)有大量文档。↩︎
  3. 求解器要求子句仅 ¬ 包含 and ∨ 运算符，因为由所有单个子句生成的公式必须采用合取范式 （CNF）。幸运的是，可以转换为 (¬a ∨ b) ， (a => b) 因此我们对布尔子句的翻译与传统的 SAT 求解器兼容。↩︎
  4. 当先前赋值的变量 A 在某个点赋值，并在以后的某个点 x 赋值时，就会触发冲突 ¬x 。这表明求解者正在探索一个导致矛盾的分支，并且应该回溯。↩