在推理图中查找第一个UIP

Question

5

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

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

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

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

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

但是，寻找支配者可能需要大量的CPU时间，我得到的印象是实用的CDCL求解器使用了一种针对此上下文的更快的算法。然而，我没有能够找到比“取第一个UIP”更具体的内容。

什么是发现第一个UIP的最佳已知算法？

- rwallace

1

我在这里找到了算法的实际描述链接，但是我没有足够的理解来用它编写答案。 - harold

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- David Eisenstat · Accepted Answer

不涉及数据结构的细节，我们有蕴含图和轨迹，它是蕴含图的拓扑排序前缀。我们想要从轨迹中弹出顶点，直到到达唯一的蕴含点 - 这将是第一个蕴含点。

通过跟踪轨迹中存在一条从最后决策文字经过v到冲突文字的路径的顶点集合v，我们识别唯一的蕴含点，其中在路径中跟随v的顶点不属于轨迹。每当该集合仅包含单个顶点时，该顶点就是唯一的蕴含点。

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

在链接网站上的示例中，该集合的演变为

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

我们报告了 x8。