强冲突分析-学习

When the 1-UIP is far from the conflict in the implication graph, the conflict clause may not be effective in preventing the SAT solver from producing many conflicts involving the same clause.

当 1-UIP 与隐含图中的冲突相距甚远时，冲突子句可能无法有效阻止 SAT 求解器产生涉及同一子句的许多冲突。

Strong conflict analysis [10] can be a remedy in such cases: It examines intermediate resolvents as UIP based conflict analysis does. Contrary to UIP-based analysis, however, it generates an additional conflict clause that contains more than one literal assigned at the current decision level.

This additional conflict clause must be one of the intermediate resolvents derived between the conflict and the 1-UIP. Usually, the closer to the conflict, the fewer literals the resolvent contains. Therefore, the additional conflict clause tends to be shorter than the conflict clause with the 1-UIP.

在这种情况下，强冲突分析[10]可以作为一种补救措施：它像基于UIP的冲突分析一样检查中间解决方案。然而，与基于 UIP 的分析相反，它会生成一个额外的冲突子句，其中包含在当前决策级别分配的多个文本。

此附加冲突条款必须是冲突和 1-UIP 之间派生的中间解决方案之一。通常，越接近冲突，解决方案包含的文字就越少。因此，附加冲突子句往往比具有 1-UIP 的冲突子句短。

We have presented a strong conflict analysis procedure for propositional satisfiability that adds more than one conflict clause from one conflict. We have shown that the additional conflict clauses help reduce the number of literals in conflict clauses as well as the depth of the implication graphs. The experimental results show large improvements compared to the state-of-the-art SAT solvers. Experimental evidence supports the claim that the performance gains are indeed due to the improved conflict analysis.

我们已经为命题可满足性提出了一个强冲突分析过程，它从一个冲突中增加了一个以上的冲突子句。我们已经表明，额外的冲突子句有助于减少冲突子句中的文字数量以及蕴涵图的深度。实验结果显示，与最先进的SAT求解器相比，有了很大的改进。实验证据支持这样的说法，即性能的提高确实是由于改进了冲突分析。

Several details of the procedure warrant further study. For instance, even though we have devised a criterion to apply the shrinking method based on the occurrence of conflicts on the same clause, the technique remains expensive in term of CPU time, and we need to investigate a more efficient way of applying it.

该程序的几个细节值得进一步研究。例如，即使我们已经设计了一个基于同一子句上冲突的发生来应用收缩方法的标准，该技术在CPU时间方面仍然是昂贵的，并且我们需要研究一种更有效的方法来应用它。

Random restart techniques have been used to enhance several SAT solvers. We conjecture that deep implication graphs and multiple conflicts on same clause make the search dwell in hot spots. Therefore in some case, restarts help the search out of a hot spot. Our strong conflict analysis should reduce the need for such random restarts.

随机重启技术已经被用于增强几个SAT求解器。我们推测深层蕴涵图和同一子句上的多重冲突使得搜索停留在热点上。因此在某些情况下，重启有助于搜索出热点。我们强大的冲突分析应该减少这种随机重启的需要。