求解器#
指南 conda install 没有详细介绍求解器黑盒。它提到了高级 Solver
API 以及 conda
如何期望从中获取事务,但我们从未了解求解器内部发生的实际情况。我们只介绍了这三个步骤
细节很复杂,但实质上,求解器将
将请求的包、命令行选项和前缀状态表达为
MatchSpec
对象查询索引以查找满足这些约束条件的最佳匹配
返回一个
PackageRecord
对象列表。
我们如何将前缀状态和配置转换为 MatchSpec
对象列表?这些如何转换为 PackageRecord
对象列表?这些 PackageRecord
对象来自哪里?我们将在这里详细介绍这些方面。
MatchSpec
与 PackageRecord
#
首先,让我们定义每个对象的作用
PackageRecord
对象代表一个具体的包压缩包及其内容。它们遵循 特定的命名约定 并公开多个字段。直接在 类代码 中查看它们。MatchSpec
对象本质上是一种查询语言,用于查找PackageRecord
对象。在内部,conda
将把您的命令行请求(如numpy>=1.19
、python=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")]
的东西?其实没那么简单。用户给出的明确指令只是我们发送给求解器的请求的一部分。其他隐含状态的信息也会被考虑在内,以构建最终的请求。也就是说,你的前缀状态也会被考虑。总而言之,求解器请求包含以下几个部分:
你环境中已经存在的包,前提是你不是在创建一个新的环境。这可以通过
conda.core.prefix_data.PrefixData
类实现,该类通过.iter_records()
方法提供迭代器。正如我们之前所看到的,它会生成conda.models.records.PrefixRecord
对象,它是已安装记录的PackageRecord
子类。你在该环境中执行过的操作;即历史记录。这是你过去所有
conda install|update|remove
命令的日志。换句话说,那些先前操作匹配的规范将在求解器中获得额外的保护。包含在强制更新列表中的包。这些包总是包含在任何请求中,以确保它们在任何情况下都能保持最新状态。
固定到特定版本的包,可以通过
.condarc
中的pinned_packages
或$PREFIX/conda-meta/pinned
文件进行定义。在新环境中,包含在
create_default_packages
列表中的包。这些规范会在每个conda create
命令中注入,因此求解器会将它们视为用户明确要求的。最后,用户请求的规范。有时它是明确的(例如
conda install numpy
),有时则隐含(例如,conda update --all
告诉求解器将所有已安装的包添加到更新列表中)。
所有这些信息来源都会生成多个 MatchSpec
对象,然后会根据命令行标志和它们来源(例如,来自固定包的规范不会被修改,除非用户明确要求)以非常具体的方式进行组合和修改。这个逻辑很复杂,将在下一节中介绍。你也可以在 技术规范:求解器状态 中找到更详细的技术描述。
conda.cli.install
中的高级逻辑#
完整的求解器逻辑并非从 conda.core.solve.Solver
API 开始,而是更早之前,一直到 conda.cli.install
模块。在这里,一些重要的决策已经做出:
是否不需要求解器,因为:
操作是明确的包安装。
用户请求回滚到历史记录检查点。
我们只是在创建现有环境的副本(克隆)。
使用哪个
repodata
源(请参见 此处)。它不仅取决于当前配置(通过.condarc
或命令行标志),还取决于use_only_tar_bz2
的值。求解器是否应该从冻结所有已安装的包开始(对于在现有环境中使用
conda install
和conda 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
。
这两种策略是叠加的,因此最终,在最终失败之前,我们将尝试四件事:
使用
current_repodata.json
和freeze_installed=True
进行求解。使用
current_repodata.json
和freeze_installed=False
进行求解。使用
repodata.json
和freeze_installed=True
进行求解。使用
repodata.json
和freeze_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
标志,允许您创建现有环境的完全可工作的副本。 这是必需的,因为您不能使用 cp
、mv
或您喜欢的文件管理器重新定位环境,否则会产生意外后果。 Conda 环境中的某些文件可能包含指向原始位置中现有文件的硬编码路径,如果使用 cp
或 mv
,这些引用将失效(但是,conda 环境可以通过 conda rename
命令重命名;有关更多信息,请参阅 以下部分)。
clone_env
函数实现了此功能。 它基本上获取源环境,生成每个已安装软件包的 URL(过滤 conda
、conda-env
及其依赖项),并将 URL 列表传递给 explicit()
。 如果源包文件不再缓存中,它将查询索引以获取当前通道的最佳匹配。 因此,副本不完全是原始环境的克隆的可能性很小。
重命名环境#
当使用 conda rename
命令重命名已存在的环境时,请记住,求解器根本不会被调用,因为该命令本质上执行了环境的 conda create --clone
和 conda remove --all
。
历史回滚#
conda install
具有一个 --revision
标志,允许您将环境状态还原到以前的状态。 这是通过 History
文件完成的,但它的 当前实现 可以被认为是错误的。 一旦修复,我们将详细介绍它。
强制移除#
与显式安装类似,您可以删除一个包而不执行完整求解。 如果 conda remove
被调用并带有 --force
,则指定的软件包将直接被删除,而不会分析它们的依赖树并修剪孤立的软件包。 这只能在查询活动前缀以获取已安装的软件包后发生,因此它在 处理 中 Solver
类。 这部分逻辑返回在过滤掉应删除的软件包后,已在 PrefixData
列表中找到的 PackageRecord
对象列表。
如果已满足,则跳过求解#
conda install
和 update
具有一个相当模糊的标志:-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
填充的全部细节在 求解器状态技术规范 中涵盖,但这里有一个关于哪些子方法参与的小地图
SolverStateContainer
的初始化:通常缩写为ssc
,它是一个辅助类,用于存储跨尝试的一些状态(请记住,有几个重试循环)。 最重要的是,它存储两个关键属性(除其他外)specs_map
:与上面相同。 这是它在求解器尝试中跨越的地方。solution_precs
:一个PackageRecord
对象列表。 它存储 SAT 求解器返回的解。 它始终初始化为反映目标前缀中已安装的软件包。
Solver._collect_all_metadata()
:使用历史记录中找到的规范或与已安装记录相对应的规范初始化specs_map
。 此方法委托给Solver._prepare()
。 这通过获取通道并减少通道来初始化索引。 然后,使用该索引创建一个conda.resolve.Resolve
实例。 索引存储在Solver
实例中,作为._index
,Resolve
对象作为._r
。 它们也保存在SolverStateContainer
中,但作为公共属性:分别为.index
和.r
。Solver._remove_specs()
:如果调用了conda remove
,它将从specs_map
中删除相关的规范。Solver._add_specs()
:对于所有其他conda
命令 (create
、install
、update
),它向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
类中的主要方法。它将执行以下操作
通过
get_reduced_index
减少索引。如果失败,尝试检测包是否丢失或请求了错误的版本。我们可以尽早引发错误以在conda.cli.install
中触发新的尝试(请记住,未冻结或下一个 repodata),或者,如果这是最后一次尝试,我们直接转到find_conflicts()
以了解问题所在。使用简化的索引实例化新的
Resolve
对象以通过gen_clauses()
生成Clauses
对象。此方法依赖于push_MatchSpec()
将MatchSpec
对象转换为Clauses
对象中的 SAT 子句(称为C
)。运行
Clauses.sat()
以解决 SAT 问题。如果找不到解决方案,则以通常的方式处理错误:尽早引发错误以触发另一次尝试或调用find_conflicts()
以尝试解释原因。如果未发现错误,则我们有了一个或多个可用解决方案,我们需要对它们进行后处理以找到最佳解决方案。这将在以下几个步骤中完成
最小化删除的包数量。SAT 子句是通过
Resolve.generate_removal_count()
生成的,然后Clauses.minimize()
将使用它来优化当前解决方案。最大化解决方案中每个记录与规范的匹配程度。SAT 子句现在在
Resolve.generate_version_metrics()
中生成。这将返回五组子句:通道、版本、构建、体系结构或非体系结构以及时间戳。此时,只优化通道和版本。最小化具有
track_feature
条目的记录数量。SAT 子句来自Resolve.generate_feature_count()
。最小化具有
features
条目的记录数量。SAT 子句来自Resolve.generate_feature_metric()
。现在,我们继续在 (2) 中开始的工作。我们将最大化构建编号,并选择体系结构特定的包而不是非体系结构变体。
我们还希望在解决方案中包含尽可能多的可选规范。由于
Resolve.generate_install_count()
生成的子句,因此对此进行了优化。同时,如果保留已安装的版本也满足请求,我们将最小化必要的更新次数。子句使用
Resolve.generate_update_count()
生成。步骤 (2) 和 (5) 也适用于间接依赖项。
最小化解决方案中的包数量。这是通过删除不必要的包来完成的。
最后,最大化时间戳,直到收敛,以便首选最新的包。
此时,SAT 解决方案索引可以转换回SAT 名称。这是在
Resolve.sat()
中找到的局部函数clean()
中完成的。我们有可能找到问题的替代解决方案,现在正在探索这一点,但最终,只有第一个解决方案将在将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 求解器是什么或做什么的细节。如果你想了解更多关于它们的信息,可以考虑查看以下资源:
Aaron Meurer 关于 Conda 内部结构的幻灯片。这些幻灯片揭示了许多关于
conda
在 2015 年的细节。有些东西已经改变了,但 SAT 求解器的核心行为仍然在那里得到了很好的解释。所有关于 Packaging-Con 2021 求解器的演讲。检查哪些演讲属于 求解器轨道,尽情享受吧!