在推理图中查找第一个 UIP

在通过冲突驱动子句学习的 SAT 求解中，每次求解器检测到一组候选变量赋值导致冲突时，它必须查看冲突的原因，从中导出子句（即整个问题的术语）并将其添加到已知子句集中。这需要在蕴涵图中选择一个切口，从中导出引理。

一种常见的方法是选择第一个唯一的蕴涵点。

如果从最新决策文字顶点到冲突顶点的所有路径都经过 l，则蕴涵图中的顶点 l 是唯一的蕴涵点（UIP）。

按照标准术语，第一个 UIP 是从冲突中回溯时遇到的第一个 UIP。

在另一种术语中，UIP 是蕴涵图上的支配者，相对于最新的决策点和冲突。因此，可以通过构建蕴涵图并使用标准算法找到支配者来找到它。

但是找到支配者可能需要大量的 cpu 时间，而且我的印象是实用的 cdcl 求解器使用特定于这种情况的更快的算法。但是，我找不到比“获取第一个 UIP”更具体的内容。

寻找第一个 UIP 的最著名算法是什么？

在不涉及数据结构细节的情况下，我们有蕴涵图和踪迹，它是蕴涵图的拓扑顺序的前缀。我们希望从轨迹中弹出顶点，直到我们到达一个独特的蕴涵点——这将是第一个。

我们通过跟踪路径中的顶点集 v 来识别唯一的隐含点，这样就存在一条从最后一个决策文字通过 v 到冲突文字的路径，其中路径中 v 之后的顶点不属于路径.每当这个集合由单个顶点组成时，该顶点就是一个唯一的蕴涵点。

最初，这个集合是两个冲突的文字，因为冲突顶点不属于路径。在集合有一个顶点之前，我们弹出最近添加到路径中的顶点 v。如果 v 属于该集合，我们将其删除并添加其前驱（丢弃重复项，natch）。

在来自链接站点的示例中，集合的演变是

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

我们报告x8。