在通过冲突驱动的子句学习进行SAT求解时，每当求解器检测到一组候选变量赋值导致冲突时，它必须找出冲突的原因，从中推导出一个子句(即整个问题的引理(，并将其添加到一组已知子句中。这需要在蕴涵图中选择一个割，从中导出引理。
一种常见的方法是选择第一个唯一的隐含点。
根据https://users.aalto.fi/~tjunttil/2020-DP-AUT/notes-sat/cdcl.html
如果从最新决策字面顶点到冲突顶点的所有路径都经过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}
并报道CCD_ 1。