求解器#

指南 conda install 没有详细介绍求解器黑盒。它提到了高级 Solver API 以及 conda 如何期望从中获取事务,但我们从未了解求解器内部发生的实际情况。我们只介绍了这三个步骤

细节很复杂,但实质上,求解器将

  1. 将请求的包、命令行选项和前缀状态表达为 MatchSpec 对象

  2. 查询索引以查找满足这些约束条件的最佳匹配

  3. 返回一个 PackageRecord 对象列表。

我们如何将前缀状态和配置转换为 MatchSpec 对象列表?这些如何转换为 PackageRecord 对象列表?这些 PackageRecord 对象来自哪里?我们将在这里详细介绍这些方面。

MatchSpecPackageRecord#

首先,让我们定义每个对象的作用

  • PackageRecord 对象代表一个具体的包压缩包及其内容。它们遵循 特定的命名约定 并公开多个字段。直接在 类代码 中查看它们。

  • MatchSpec 对象本质上是一种查询语言,用于查找 PackageRecord 对象。在内部,conda 将把您的命令行请求(如 numpy>=1.19python=3.*pytorch=1.8.*=*cuda*)转换为此类的实例。此查询语言有自己的语法和规则,此处 详细介绍。MatchSpec 对象最重要的字段是

    • name:包的名称(例如 pytorch);始终预期。

    • version:版本约束(例如 1.8.*);可以为空,但如果设置了 build,则将其设置为 * 以避免出现 .conda_build_form() 方法的问题。

    • build:构建字符串约束(例如 *cuda*);可以为空。

从 PackageRecord 实例创建 MatchSpec 对象

您可以使用 .to_match_spec() 方法从 PackageRecord 实例创建 MatchSpec 对象。这将创建一个 MatchSpec 对象,其字段设置为完全匹配原始 PackageRecord

请注意,有两个 PackageRecord 子类具有额外的字段,因此我们需要区分三种类型,它们都有用

  • PackageRecord:索引(频道)中存在的记录。

  • PackageCacheRecord:已在缓存中提取的记录。包含有关磁盘上的压缩包路径及其提取目录的额外字段。

  • PrefixRecord:安装在特定前缀中的记录。与上面相同,此外还包含构成包的文件以及它们如何在特定前缀中链接的信息。它还可以保存有关哪个 MatchSpec 字符串导致安装此记录的信息。

远程状态:索引#

因此,求解器将 MatchSpec 对象作为输入,查询索引以查找最佳匹配,并返回 PackageRecord 对象。完美。什么是索引?它是将请求的 conda 频道聚合到一个实体中所产生的结果。有关更多信息,请查看 获取索引.

本地状态:前缀和上下文#

当你执行 conda install numpy 时,你是否认为求解器只会看到类似 specs=[MatchSpec("numpy")] 的东西?其实没那么简单。用户给出的明确指令只是我们发送给求解器的请求的一部分。其他隐含状态的信息也会被考虑在内,以构建最终的请求。也就是说,你的前缀状态也会被考虑。总而言之,求解器请求包含以下几个部分:

  1. 你环境中已经存在的包,前提是你不是在创建一个新的环境。这可以通过 conda.core.prefix_data.PrefixData 类实现,该类通过 .iter_records() 方法提供迭代器。正如我们之前所看到的,它会生成 conda.models.records.PrefixRecord 对象,它是已安装记录的 PackageRecord 子类。

  2. 你在该环境中执行过的操作;即历史记录。这是你过去所有 conda install|update|remove 命令的日志。换句话说,那些先前操作匹配的规范将在求解器中获得额外的保护。

  3. 包含在强制更新列表中的包。这些包总是包含在任何请求中,以确保它们在任何情况下都能保持最新状态。

  4. 固定到特定版本的包,可以通过 .condarc 中的 pinned_packages$PREFIX/conda-meta/pinned 文件进行定义。

  5. 在新环境中,包含在 create_default_packages 列表中的包。这些规范会在每个 conda create 命令中注入,因此求解器会将它们视为用户明确要求的。

  6. 最后,用户请求的规范。有时它是明确的(例如 conda install numpy),有时则隐含(例如,conda update --all 告诉求解器将所有已安装的包添加到更新列表中)。

所有这些信息来源都会生成多个 MatchSpec 对象,然后会根据命令行标志和它们来源(例如,来自固定包的规范不会被修改,除非用户明确要求)以非常具体的方式进行组合和修改。这个逻辑很复杂,将在下一节中介绍。你也可以在 技术规范:求解器状态 中找到更详细的技术描述。

../../_images/solver-deep-dive-1.png

局部变量会显式和隐式地影响求解过程。正如在 conda install 深入探究 中所见,主要参与者是 conda.core.solve.Solver 类。在调用 SAT 求解器之前,我们可以描述九个步骤:#

  1. 使用用户请求的包和活动环境(目标前缀)实例化 Solver 类。

  2. 在实例上调用 solve_for_transaction() 方法,该方法会调用 solve_for_diff()

  3. 调用 solve_final_state(),该方法会从 CLI 获取一些其他参数。

  4. 在某些情况下,我们可以提前返回(例如,包已经安装)。

  5. 如果我们没有提前返回,我们将收集所有局部变量到一个 MatchSpec 对象列表中。

对于步骤六到九,请参见 此图

../../_images/solver-deep-dive-2.png

求解中的远程变量本质上指的是包索引(通道)。此图描述了九个步骤,重点关注 6-9。对于步骤 1-5,请参见 上一图#

  1. 现在需要获取所有通道,但需要对它们进行聚合和缩减,以便求解器只处理相关部分。此步骤将“通道”转换为可用 PackageRecord 对象列表。

  2. 这就是 SAT 求解器发挥作用的地方。它将使用 MatchSpec 对象列表从索引中选择多个 PackageRecord 条目,从而构建“已解决环境的最终状态”。这将在本深入探究指南的后面详细介绍,如果你需要更多信息。

  3. solve_for_diff 会获取最终状态并将其与初始状态进行比较,生成它们之间的差异(例如,包 A 已更新到版本 1.2,包 B 已删除)。

  4. solve_for_transaction 会获取差异以及实例中的一些其他元数据,以生成 Transaction 对象。

conda.cli.install 中的高级逻辑#

完整的求解器逻辑并非从 conda.core.solve.Solver API 开始,而是更早之前,一直到 conda.cli.install 模块。在这里,一些重要的决策已经做出:

  • 是否不需要求解器,因为:

    • 操作是明确的包安装。

    • 用户请求回滚到历史记录检查点。

    • 我们只是在创建现有环境的副本(克隆)。

  • 使用哪个 repodata 源(请参见 此处)。它不仅取决于当前配置(通过 .condarc 或命令行标志),还取决于 use_only_tar_bz2 的值。

  • 求解器是否应该从冻结所有已安装的包开始(对于在现有环境中使用 conda installconda remove 的默认设置)。

  • 如果求解器找不到解决方案,我们是否需要在不冻结当前 repodata 变体的已安装包的情况下再次尝试,或者是否应该尝试使用下一个 repodata

因此,大体上,那里的全局逻辑遵循以下伪代码:

if operation in (explicit, rollback, clone):
    transaction = handle_without_solver()
else:
    repodatas = from_config or ("current_repodata.json", "repodata.json")
    freeze = (is_install or is_remove) and env_exists and update_modifier not in argv
    for repodata in repodatas:
        try:
            transaction = solve_for_transaction(...)
        except:
            if repodata is last:
                raise
            elif freeze:
                transaction = solve_for_transaction(freeze_installed=False)
            else:
                continue  # try next repodata

handle_txn(transaction)

查看 此图 以了解此伪代码的示意图。

然后,我们有两个原因需要重新运行完整的求解器逻辑:

  • 冻结已安装的包没有成功,因此我们尝试不冻结再次尝试。

  • 使用 current_repodata 没有成功,因此我们尝试使用完整的 repodata

这两种策略是叠加的,因此最终,在最终失败之前,我们将尝试四件事:

  1. 使用 current_repodata.jsonfreeze_installed=True 进行求解。

  2. 使用 current_repodata.jsonfreeze_installed=False 进行求解。

  3. 使用 repodata.jsonfreeze_installed=True 进行求解。

  4. 使用 repodata.jsonfreeze_installed=False 进行求解。

有趣的是,这些策略旨在提高 conda 的平均性能,但应该将它们视为冒险的赌注。这些尝试可能会很昂贵!

如何请求更简单的方案

如果你想尝试完整方案,而不检查优化求解方案是否有效,你可以在 conda install 命令中使用以下标志覆盖默认行为:

  • --repodata-fn=repodata.json:不使用 current_repodata.json

  • --update-specs:不尝试冻结已安装的包。

然后,Solver 类有它自己的内部逻辑,其中也包含一些重试循环。这将在后面进行讨论并总结。

提前退出任务#

有些任务根本不涉及求解器。让我们列举一下:

  • 明确的包安装:不需要索引或前缀状态。

  • 克隆环境:如果缓存已清除,则可能需要索引。

  • 历史记录回滚:当前已损坏。

  • 强制移除:需要前缀状态。这发生在 Solver 类中。

  • 如果已满足,则跳过求解:需要前缀状态。这发生在 Solver 类中。

明确的包安装#

这些命令不需要求解器,因为请求的包是用指向特定压缩包的直接 URL 或路径表示的。我们已经有了类似 PackageRecord 的实体,而不是 MatchSpec!为了使这能够工作,所有请求的包都需要是 URL 或路径。它们可以在命令行中键入,也可以在包含 @EXPLICIT 行的文本文件中键入。

由于求解器没有参与,因此不会处理显式包的依赖项。这可能会使环境处于不一致状态,可以通过运行 conda update --all 来解决,例如。

明确的安装由 explicit 函数处理。

克隆环境#

conda create 具有一个 --clone 标志,允许您创建现有环境的完全可工作的副本。 这是必需的,因为您不能使用 cpmv 或您喜欢的文件管理器重新定位环境,否则会产生意外后果。 Conda 环境中的某些文件可能包含指向原始位置中现有文件的硬编码路径,如果使用 cpmv,这些引用将失效(但是,conda 环境可以通过 conda rename 命令重命名;有关更多信息,请参阅 以下部分)。

clone_env 函数实现了此功能。 它基本上获取源环境,生成每个已安装软件包的 URL(过滤 condaconda-env 及其依赖项),并将 URL 列表传递给 explicit()。 如果源包文件不再缓存中,它将查询索引以获取当前通道的最佳匹配。 因此,副本不完全是原始环境的克隆的可能性很小。

重命名环境#

当使用 conda rename 命令重命名已存在的环境时,请记住,求解器根本不会被调用,因为该命令本质上执行了环境的 conda create --cloneconda remove --all

历史回滚#

conda install 具有一个 --revision 标志,允许您将环境状态还原到以前的状态。 这是通过 History 文件完成的,但它的 当前实现 可以被认为是错误的。 一旦修复,我们将详细介绍它。

强制移除#

与显式安装类似,您可以删除一个包而不执行完整求解。 如果 conda remove 被调用并带有 --force,则指定的软件包将直接被删除,而不会分析它们的依赖树并修剪孤立的软件包。 这只能在查询活动前缀以获取已安装的软件包后发生,因此它在 处理Solver 类。 这部分逻辑返回在过滤掉应删除的软件包后,已在 PrefixData 列表中找到的 PackageRecord 对象列表。

如果已满足,则跳过求解#

conda installupdate 具有一个相当模糊的标志:-S, --satisfied-skip-solve

如果请求的规范满足,则尽早退出,不要运行求解器。 还跳过由“aggressive_update_packages”配置的积极更新。 与“pip install”的默认行为类似。

这也是在 实现Solver 级别,因为我们还需要一个 PrefixData 实例。 它本质上检查所有传递的 MatchSpec 对象是否可以匹配前缀中已存在的 PackageRecord。 如果是这种情况,我们将按原样返回已安装的状态。 如果不是,我们将继续进行完整求解。

Solver.solve_final_state() 的详细信息#

注意

从这里开始,文档只涵盖经典求解器逻辑(使用 pycosat)。 libmamba 求解器具有不同的方法,这里没有记录。 有关更多信息,请参阅 其文档

这是 conda 逻辑的大部分复杂之处定义的地方。 在此步骤中,配置、命令行标志、用户请求的规范和前缀状态被聚合以查询当前索引以获取最佳匹配。

所有这些状态位的聚合将生成一个 MatchSpec 对象列表。 虽然很容易确定哪些软件包名称将进入列表,但决定规范携带哪些版本和构建字符串约束要复杂一些。

这目前在 conda.core.solve.Solver 类中实现。 它的主要目标是填充 specs_map 字典,该字典将软件包名称 (str) 映射到 MatchSpec 对象。 这是在 .solve_final_state() 方法的开头发生的。 specs_map 填充的全部细节在 求解器状态技术规范 中涵盖,但这里有一个关于哪些子方法参与的小地图

  1. SolverStateContainer 的初始化:通常缩写为 ssc,它是一个辅助类,用于存储跨尝试的一些状态(请记住,有几个重试循环)。 最重要的是,它存储两个关键属性(除其他外)

    • specs_map:与上面相同。 这是它在求解器尝试中跨越的地方。

    • solution_precs:一个 PackageRecord 对象列表。 它存储 SAT 求解器返回的解。 它始终初始化为反映目标前缀中已安装的软件包。

  2. Solver._collect_all_metadata():使用历史记录中找到的规范或与已安装记录相对应的规范初始化 specs_map。 此方法委托给 Solver._prepare()。 这通过获取通道并减少通道来初始化索引。 然后,使用该索引创建一个 conda.resolve.Resolve 实例。 索引存储在 Solver 实例中,作为 ._indexResolve 对象作为 ._r。 它们也保存在 SolverStateContainer 中,但作为公共属性:分别为 .index.r

  3. Solver._remove_specs():如果调用了 conda remove,它将从 specs_map 中删除相关的规范。

  4. Solver._add_specs():对于所有其他 conda 命令 (createinstallupdate),它向 specs_map 添加(或修改)相关的规范。 这是类中最复杂的部分逻辑之一!

检查求解器 API 的其他部分

您可以 在这里 检查求解器 API 的其余部分。

此时,specs_map 已充分填充,我们可以调用由 conda.resolve.Resolve 类包装的 SAT 求解器。 这是在 Solver._run_sat() 中完成的,但此方法在实际解决 SAT 问题之前会做一些其他事情

  • 在调用 ._run_sat() 之前,将通过 Solver._find_inconsistent_packages 执行不一致性分析。 如果 Resolve.bad_installed() 确定它们会导致不一致,这将抢先从 ssc.solution_precs 中删除某些 PackageRecord 对象。 这实际上运行了一系列小型求解来检查已安装的记录是否形成可满足的子句集。 那些阻止找到该解决方案的记录将被标注为这样,并在以后的实际求解过程中被忽略。

  • 确保索引中存在请求的软件包名称。

  • 预测并尽量减少潜在的冲突规范。 这是在一个由 Resolve.get_conflicting_specs() 驱动的 while 循环中发生的。 如果发现某个规范存在冲突,则对其进行“中和”:创建一个新的 MatchSpec 对象,但没有版本和构建字符串约束(例如 numpy >=1.19 变成 numpy)。 然后,再次调用 Resolve.get_conflicting_specs(),循环继续,直到收敛:冲突列表不能再减少,要么是因为没有冲突,要么是因为现有的冲突无法通过约束松弛来解决。

  • 现在,调用 SAT 求解器。 这是通过 Resolve.solve() 完成的。 有关更多信息,请参见下文。

  • 如果求解器失败,则会引发 UnsatisfiableError。 根据我们所处的哪个尝试,conda 将尝试使用非冻结的已安装软件包或不同的 repodata 再次尝试,或者它将放弃并分析冲突原因核心。 这将在后面详细介绍。

  • 如果求解器成功,则需要执行一些簿记

    • 恰好出现在历史记录中的中和规范会被标注为这样。

    • 不一致的包被添加回解决方案中,包括潜在的孤儿包。

    • 约束分析通过 Solver.get_constrained_packages()Solver.determine_constricting_specs() 来运行,帮助用户理解为什么一些包没有更新。

不过,我们还没有完成。在 Solver._run_sat() 之后,我们仍然需要运行解算器后逻辑!解算后,最终的 PackageRecord 对象列表可能还会改变,如果设置了某些修饰符。这在 Solver._post_sat_handling() 中处理。

  • --no-deps (DepsModifier.NO_DEPS):从最终解决方案中删除显式请求的包的依赖项。

  • --only-deps (DepsModifier.ONLY_DEPS):从最终解决方案中删除显式请求的包,但保留它们的依赖项。这是通过 PrefixGraph.remove_youngest_descendant_nodes_with_specs() 完成的。

  • --update-deps (UpdateModifier.UPDATE_DEPS):这是最有趣的一个。它实际上运行第二个解算(!),其中用户请求的规范是最初请求的规范加上它们的(现在确定的)依赖项。

  • --prune:从解决方案中删除孤儿包。

解算器还检查 Conda 更新。

有趣的是,解算器 API 也负责检查配置的通道中是否有新的 conda 版本可用。这是在这里完成的,以利用索引已经为该类的其余部分构建的事实。

关于 conda.resolve.Resolve 的详情#

这是实际包装 SAT 解算器的类。 conda.core.solve.Solver 是一个更高层次的 API,它配置解算器的请求并准备事务。实际的解决方案是在我们现在讨论的这个其他模块中计算的。

Resolve 对象主要接收两个参数。

  • 已获取的 index,由 conda.index.get_index() 处理。

  • 配置的 channels,以便可以对通道优先级进行排序。

它还会保存某些状态。

  • index 将在 .groups 字典 (str, [PackageRecord]) 下按名称分组。每个组之后都会被排序,以便较新的包排在前面,这有助于更好地减少索引。

  • 将创建另一个 PackageRecord 组的字典,其键值为它们的 track_features 条目,位于 .trackers 属性下。

  • 其他一些字典被初始化为缓存。

此类中的主要方法是

  • bad_installed():此方法使用一系列小型解算来检查已安装的包是否处于一致状态。换句话说,如果所有 PackageRecord 条目都被表示为 MatchSpec 对象,环境是否可以解算?

  • get_reduced_index():此方法获取完整索引并修剪当前请求不需要的部分,从而减小解决方案空间并加速解算器。

  • gen_clauses():这将实例化和配置 Clauses 对象,这是实际的 SAT 解算器包装器。稍后将详细介绍。

  • solve()Resolve 类中的主要方法。它将在下一节中讨论。

  • find_conflicts():如果解算器没有成功,此方法将执行冲突分析以找到当前冲突的最合理解释。它本质上依赖于 build_conflict_map() 来“找到可能导致冲突的共同依赖项”。 conda 可能在此方法中花费大量时间。

禁用冲突分析

可以通过 context.unsatisfiable_hints 选项禁用冲突分析,但不幸的是,这会妨碍 conda 的迭代逻辑。它将尽早从尝试链中跳过,并阻止解算器尝试约束更少的规范。这是应该改进的逻辑的一部分。

Resolve.solve()#

如上所述,这是 Resolve 类中的主要方法。它将执行以下操作

  1. 通过 get_reduced_index 减少索引。如果失败,尝试检测包是否丢失或请求了错误的版本。我们可以尽早引发错误以在 conda.cli.install 中触发新的尝试(请记住,未冻结或下一个 repodata),或者,如果这是最后一次尝试,我们直接转到 find_conflicts() 以了解问题所在。

  2. 使用简化的索引实例化新的 Resolve 对象以通过 gen_clauses() 生成 Clauses 对象。此方法依赖于 push_MatchSpec()MatchSpec 对象转换为 Clauses 对象中的 SAT 子句(称为 C)。

  3. 运行 Clauses.sat() 以解决 SAT 问题。如果找不到解决方案,则以通常的方式处理错误:尽早引发错误以触发另一次尝试或调用 find_conflicts() 以尝试解释原因。

  4. 如果未发现错误,则我们有了一个或多个可用解决方案,我们需要对它们进行后处理以找到最佳解决方案。这将在以下几个步骤中完成

    1. 最小化删除的包数量。SAT 子句是通过 Resolve.generate_removal_count() 生成的,然后 Clauses.minimize() 将使用它来优化当前解决方案。

    2. 最大化解决方案中每个记录与规范的匹配程度。SAT 子句现在在 Resolve.generate_version_metrics() 中生成。这将返回五组子句:通道、版本、构建、体系结构或非体系结构以及时间戳。此时,只优化通道和版本。

    3. 最小化具有 track_feature 条目的记录数量。SAT 子句来自 Resolve.generate_feature_count()

    4. 最小化具有 features 条目的记录数量。SAT 子句来自 Resolve.generate_feature_metric()

    5. 现在,我们继续在 (2) 中开始的工作。我们将最大化构建编号,并选择体系结构特定的包而不是非体系结构变体。

    6. 我们还希望在解决方案中包含尽可能多的可选规范。由于 Resolve.generate_install_count() 生成的子句,因此对此进行了优化。

    7. 同时,如果保留已安装的版本也满足请求,我们将最小化必要的更新次数。子句使用 Resolve.generate_update_count() 生成。

    8. 步骤 (2) 和 (5) 也适用于间接依赖项。

    9. 最小化解决方案中的包数量。这是通过删除不必要的包来完成的。

    10. 最后,最大化时间戳,直到收敛,以便首选最新的包。

  5. 此时,SAT 解决方案索引可以转换回SAT 名称。这是在 Resolve.sat() 中找到的局部函数 clean() 中完成的。

  6. 我们有可能找到问题的替代解决方案,现在正在探索这一点,但最终,只有第一个解决方案将在将SAT 名称转换为 PackageRecord 对象时返回。

Clauses 对象使用多层包装 SAT 解算器#

Resolve 类公开了解算逻辑,但当涉及与 SAT 解算器引擎交互时,这是通过 Clauses 对象树完成的。我们之所以说“树”,是因为实际的引擎被包装在多层中

  • Resolve 根据需要生成 conda.common.logic.Clauses 对象。

  • Clauses 是其私有 conda.common._logic.Clauses 对等对象的紧密包装器。我们称前者为 _Clauses。它只是使用 ._eval() 调用和其他快捷方式来包装 _Clauses API,以方便使用。

  • _Clauses 提供了一个 API 来处理原始 SAT 公式或子句。它将包装一个 conda.common._logic._SatSolver 子类。这些是包装 SAT 解算器引擎的子类!到目前为止,有三个子类,可以通过 context.sat_solver 设置进行选择

    • _PycoSatSolver,键为 pycosat。这是默认的求解器,它是 围绕 picosat 项目 的 Python 包装器。

    • _PySatSolver,键为 pysat。使用 pysat 项目 中的 Glucose4 求解器。

    • _PyCryptoSatSolver,键为 pycryptosat。使用 CryptoMiniSat 项目 的 Python 绑定。

原则上,如果使用订阅 _SatSolver API 的包装器,可以将更多 SAT 求解器添加到 conda 中。但是,如果原因是选择性能更好的引擎,请考虑以下几点:

  • 已包装的 SAT 求解器已经在使用编译语言。

  • 生成子句确实是用纯 Python 编写的,并且具有非平凡的开销。

  • 如果“赌注”不成功,像减少索引和约束解空间这样的优化技巧会付出代价。

关于一般 SAT 求解器的更多信息

本指南没有涵盖 SAT 求解器是什么或做什么的细节。如果你想了解更多关于它们的信息,可以考虑查看以下资源:

../../_images/solver-deep-dive-3.png

在这里你可以看到高级 Solver API 如何与低级 Resolve 和 Clauses 对象交互。#

CLI 报告中的“收集元数据”步骤仅编译来自 CLI 参数、前缀状态和所选通道的必要信息,为 SAT 求解器适配器提供两条关键信息:

  • MatchSpec 对象列表(“用户想要在该环境中得到什么”)

  • PackageRecord 对象列表(“通道中可用的软件包”)

因此,本质上,SAT 求解器使用 MatchSpec 对象来选择哪些 PackageRecord 对象以最佳方式满足用户请求。必要的计算是 CLI 报告中“解决环境……”步骤的一部分。