在推理图中找到第一个 UIP
Finding the first UIP in an inference graph
在通过冲突驱动子句学习解决 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 是蕴涵图上相对于最新决策点和冲突的支配者。因此，可以通过构建蕴涵图并使用标准算法寻找支配者来找到它。
但是寻找支配者可能会花费大量 CPU 时间，而且我的印象是实用的 CDCL 求解器使用特定于此上下文的更快算法。但是，我找不到比 'take the first UIP'.
更具体的内容
找到第一个 UIP 的最著名算法是什么？
在不讨论数据结构细节的情况下，我们有蕴涵图和踪迹，它是蕴涵图的拓扑顺序的前缀。我们想要从轨迹中弹出顶点，直到我们到达一个唯一的蕴涵点——这将是第一个。
我们通过跟踪路径中的顶点集v来识别唯一蕴涵点，使得存在从最后一个决策文字通过v到冲突文字的路径，其中路径中v之后的顶点不属于踪迹。每当这个集合由一个顶点组成时，该顶点就是一个唯一的蕴涵点。
最初，这个集合是两个冲突的文字，因为冲突的顶点不属于轨迹。直到集合有一个顶点，我们弹出最近添加到轨迹的顶点 v。如果 v 属于该集合，我们将其删除并添加其前身（丢弃重复项，natch）。
在链接站点的示例中，集合的演变是
{x11, -x12}
{x10, x11}
{-x9, x10}
{x8, -x9}
{x8}
我们报告 x8。
在通过冲突驱动子句学习解决 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 是蕴涵图上相对于最新决策点和冲突的支配者。因此，可以通过构建蕴涵图并使用标准算法寻找支配者来找到它。
但是寻找支配者可能会花费大量 CPU 时间，而且我的印象是实用的 CDCL 求解器使用特定于此上下文的更快算法。但是，我找不到比 'take the first UIP'.
更具体的内容找到第一个 UIP 的最著名算法是什么？
在不讨论数据结构细节的情况下，我们有蕴涵图和踪迹，它是蕴涵图的拓扑顺序的前缀。我们想要从轨迹中弹出顶点，直到我们到达一个唯一的蕴涵点——这将是第一个。
我们通过跟踪路径中的顶点集v来识别唯一蕴涵点，使得存在从最后一个决策文字通过v到冲突文字的路径，其中路径中v之后的顶点不属于踪迹。每当这个集合由一个顶点组成时，该顶点就是一个唯一的蕴涵点。
最初，这个集合是两个冲突的文字，因为冲突的顶点不属于轨迹。直到集合有一个顶点，我们弹出最近添加到轨迹的顶点 v。如果 v 属于该集合，我们将其删除并添加其前身（丢弃重复项，natch）。
在链接站点的示例中，集合的演变是
{x11, -x12}
{x10, x11}
{-x9, x10}
{x8, -x9}
{x8}
我们报告 x8。