查找推理图中的第一个 UIP

Question

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

执行此操作的常见方法是选择第一个唯一蕴含点。

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

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

用替代术语来说，UIP 是蕴含图上相对于最新决策点和冲突的主导者。因此，可以通过构建蕴含图并使用标准算法来查找支配者来找到它。

但寻找支配者可能会花费大量的 CPU 时间，而且我的印象是实用的 CDCL 求解器使用特定于此上下文的更快算法。然而，我找不到比“获取第一个 UIP”更具体的内容。

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

Answer 1

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

\n

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

\n

最初，该集合是两个冲突的文字，因为冲突顶点不属于路径。直到该集合有一个顶点为止，我们弹出最近添加到轨迹中的顶点 v。如果 v 属于该集合，我们将删除它并添加它的前任（自然地丢弃重复项）。

\n

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

\n

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

我们报告x8。

\n