Speedup Techniques Utilized in Modern SAT Solvers −An Analysis in the MIRA Environment
Lewis M.D.T., Schubert T., Becker B.W. (2005) Speedup Techniques Utilized in Modern SAT Solvers. In: Bacchus F., Walsh T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg
| This paper describes and compares features and techniques modern SAT solvers utilize to maximize performance. Here we focus on: Implication Queue Sorting (IQS) combined with Early Conflict Detection Based BCP (ECDB); and a modified decision heuristic based on the combination of Variable State Independent Decaying Sum (VSIDS), Berkmin, and Siege’s Variable Move to Front (VMTF). These features were implemented and compared within the framework of the MIRA SAT solver. The efficient implementation and analysis of these features are presented and the speedup and robustness each feature provides is demonstrated. Finally, with everything enabled (ECDB with IQS and advanced decision heuristics), MIRA was able to consistently outperform zChaff and even Forklift on the benchmarks provided, solving 37 out of 111 industrial benchmarks compared to zChaff’s 21 and Forklift’s 28. |
|
译文：本文描述和比较了现代SAT求解器用来最大化性能的特性和技术。
|
| 译文：这些特性是在MIRA SAT求解器的框架内实现和比较的。译文：给出了这些特性的有效实现和分析，并演示了每个特性所提供的加速和鲁棒性。 |
| 译文：最后，在所有功能都被激活的情况下(具有蕴含队列排序和高级决策启发式的ECDB)， MIRA能够在所提供的基准测试中始终超过zChaff甚至Forklift，在111个工业基准测试中解决了37个，而zChaff是21个，Forklift是28个。 |
|
SAT solvers have advanced considerably since the days of the original Davis-Putnam (DP) algorithm [5,6]. While the underlying algorithm has not changed, improvements in its implementation have made it practical. SAT solvers are now commonly used in industrial fields such as EDA. Such features as Early Conflict Detection BCP (ECDB) [4], Conflict Analysis [7], watched literals [1,21], advanced decision heuristics, and others are what have made SAT solvers practical. Now, while these techniques are powerful, they must all be used together in unison, increasing the complexity of modern SAT solvers. This paper tries to clarify and explain many of the features found in modern SAT solvers while including features only found in our MIRA solver such as the novel Implication Queue Sorting (IQS). 译文：本文试图阐明和解释在现代SAT求解器中发现的许多特征，同时包括仅在我们的MIRA求解器中发现的特征，如新的隐含队列排序(IQS)。 |
| The next section focuses on IQS followed by a section on ECDB. Section 4 will discuss the novel hybrid decision heuristic used in MIRA and how random restarts can be used. Section 5 covers conflict analysis and conflict clause database management. After presenting the parts of a solver, a comparison of MIRA and other solvers on Industrial and Handmade benchmarks are given. Lastly, this paper assumes the reader has a good understanding of the inner workings of a SAT solver and it therefore will not present an overview of current SAT solvers. An overview can be found in [16]. |
|
Before discussing IQS and ECDB directly, it is important to understand some of the reasons for using it. The idea behind ECDB is to find good conflicts while reducing the work the BCP procedure must do in order to find them. However, in most solvers the BCP procedure checks many clauses that will rarely or never lead to a conflict. This is inefficient and slows down the solver. 译文：在直接讨论IQS和ECDB之前，了解使用它的一些原因是很重要的。ECDB背后的想法是找到好的冲突，同时减少BCP过程为了找到它们而必须做的工作。然而，在大多数解决方案中，BCP过程检查许多很少或永远不会导致冲突的子句。这是低效的，并且会降低求解器的速度。 |
|
Normally, the BCP starts by checking all clauses that contain the current decision variable as a watched literal. As it checks these clauses, it will normally find many implications that it will add to the implication queue. When it is done checking the current decision variable it will move on and check the first implication in the implication queue. The problem with this method is that the BCP procedure will check many implications that are unrelated to the current search space. So, to try and reduce the number of implications the BCP must process, MIRA introduces Implication Queue Sorting (IQS). Simply put, the BCP procedure in MIRA uses a heuristic to select which implications to check first from the implication queue. This is in contrast to other solvers which process the implication queue in chronological order. This results in a significant speedup. 译文：BCP首先检查所有包含当前决策变量的子句，这些子句作为被观察的文字。译文：在检查这些子句时，它通常会发现许多蕴含文字并将它们添加到蕴含队列队列之中。译文：检查完当前决策变量后，它将继续检查蕴含队列中的第一个蕴含文字。译文：这种方法的问题是，BCP过程将检查许多与当前搜索空间无关的蕴含文字。 译文：MIRA引入了隐含队列排序(IQS)。简单地说，MIRA中的BCP过程使用启发式从隐含队列中选择首先检查的隐含。这与其他按时间顺序处理隐含队列的解决方案形成了对比。这将导致显著的加速。 |
| However, to realize this speedup, IQS must be implemented efficiently as it is an operation that is performed frequently. Implications are added and removed from the queue often, the queue can grow quite large (100’s of implications), and is reset after every conflict. In MIRA, a reverse VSIDS algorithm is used when selecting the implication to check next.译文：在选择下一步要检查的含义时，使用反向VSIDS算法。 Instead of taking the literal with highest score, MIRA selects the literal whose complement has the highest score (using the same VSIDS counters as the decision heuristic). 译文：MIRA没有选择得分最高的文字，而是选择其补语得分最高的文字。The idea is that as soon as the BCP starts, the solver is now trying to find a conflict, not solve the problem.译文：这种想法是，一旦BCP启动，解决者就会试图找到冲突，而不是解决问题。 |
原文：https://www.cnblogs.com/yuweng1689/p/13151774.html