algorithm - 在推理图中查找第一个 UIP

Question

在通过冲突驱动子句学习的 SAT 求解中，每次求解器检测到一组候选变量赋值导致冲突时，它必须查看冲突的原因，从中导出一个子句(即根据整体问题)并将其添加到已知子句集中。这需要在蕴涵图中选择一个切口，从中导出引理。
一种常见的方法是选择第一个唯一的蕴涵点。
每 https://users.aalto.fi/~tjunttil/2020-DP-AUT/notes-sat/cdcl.html

A vertex l in the implication graph is a unique implication point (UIP) if all the paths from the latest decision literal vertex to the conflict vertex go through l.

标准术语中的第一个 UIP 是从冲突中回溯时遇到的第一个 UIP。
在替代术语中，相对于最新决策点和冲突，UIP 是蕴涵图上的支配者。因此，可以通过构建蕴涵图并使用标准算法来找到支配者。
但是找到支配者可能需要大量的 CPU 时间，而且我的印象是实用的 CDCL 求解器使用特定于这种情况的更快的算法。但是，我找不到比“采取第一个 UIP”更具体的内容。
寻找第一个 UIP 的最著名算法是什么？

Answer 1

在不涉及数据结构细节的情况下，我们有蕴涵图和踪迹，它是蕴涵图的拓扑顺序的前缀。我们想从轨迹中弹出顶点，直到我们到达一个独特的蕴涵点——这将是第一个。
我们通过跟踪路径中的顶点集 v 来识别唯一的隐含点，从而存在从最后一个决策文字通过 v 到冲突文字的路径，其中路径中 v 之后的顶点不属于路径。每当该集合由单个顶点组成时，该顶点就是唯一的蕴涵点。
最初，这个集合是两个冲突的文字，因为冲突顶点不属于路径。在集合有一个顶点之前，我们弹出最近添加到路径中的顶点 v。如果 v 属于该集合，我们将其删除并添加其前驱(丢弃重复项，natch)。
在链接站点的示例中，集合的演变是

{x11, -x12}
{x10, x11}
{-x9, x10}
{x8, -x9}
{x8}

我们报告 x8 .