Many state-of-the-art SAT solvers use the VSIDS heuristic to make branching decisions based on the activity of variables or literals. In combination with rapid restarts and phase saving this yields a powerful decision heuristic in practice. However, there are approaches that motivate more in-depth reasoning to guide the search of the SAT solver. But more reasoning often requires more information and comes along with more complex data structures. This may sometimes even cause strong concepts to be inapplicable in practice.

译文：然而，有一些方法可以激发更深入的推理来指导SAT求解器的搜索。

译文：但更多的推理往往需要更多的信息，并伴随着更复杂的数据结构。这有时甚至可能导致强概念在实践中不适用。

In this paper we present a suitable data structure for the DMRP approach to overcome the problem above. Moreover, we show how DMRP can be combined with CDCL solving to be competitive to state-of-the-art solvers and to even improve on some families of industrial instances.

译文：在本文中，我们提出了一个适用于DMRP方法的数据结构来克服上述问题。

译文：此外，我们还展示了如何将DMRP与CDCL解决方案结合在一起，以便与最先进的解决方案相竞争，甚至改进一些工业实例系列。

Research in satisfiability checking (SAT) has managed to bridge the gap between theory and practice in many aspects. There are several kinds of real-world problems that are actually tackled by modelling those problems as SAT instances like hardware and software verification [21,10], planning [11], automotive product configuration [13] and haplotype inference in bioinformatics [15] (cf. [16]).

译文：可满足性检验的研究在许多方面弥补了理论与实践的差距。译文：通过将这些问题建模为SAT实例，实际上可以解决几种实际问题，如硬件和软件验证[21,10]、规划[11]、汽车产品配置[13]和生物信息学[15]中的单倍型推断(cf.[16])。

In the domain of SAT solving there are different schemes and even more variants of these schemes to decide whether there exists a satisfying assignment to the variables of a Boolean formula in CNF or if a formula cannot be satisfied by any assignment.译文：在SAT求解的领域中，有不同的方案，甚至这些方案的变种，以决定是否存在一个布尔公式的变量分配CNF或如果一个公式不能满足分配。

Both experiments and applications show that there is no perfect SAT solving approach that is suited for all different categories and families of problem instances. 译文：实验和应用表明，没有一种完美的SAT解决方法适合所有不同类别和家庭的问题实例。

However, conflict-driven solving has proven itself to be very successful on a wide range of benchmarks. In this paper we study the quite new DMRP algorithm (decision making with a reference point) [8,9] from a practical point of view. Moreover, a hybrid approach that combines DMRP and CDCL solving is presented which is also motivated by experimental evaluations.

Conflict-Driven Solving.

Conflict-driven solving with clause learning (CDCL) is a leading approach and is especially but not only successful for industrial problems. It is based on the GRASP algorithm [17] which extends the original DPLL branch-and-bound procedure [5,4] by the idea of learning from conflicting assignments.

Moreover, conflicts are analysed to jump over parts of the search space that would cause further conflicts. 此外，对冲突进行分析，以跳过搜索空间中可能导致进一步冲突的部分。

There are several improvements to the original algorithm like the two-watched-literal data structure and the VSIDS (variable state independent decaying sum) variable selection heuristic [18].

In recent years further improvements have been achieved by developing different restart strategies like the concept of rapid and adaptive restarts [3,2] and so-called Luby restarts [14].

In combination with phase-saving [19] frequent restarts constitute a strong concept especially for industrial SAT instances.

此外，对冲突进行分析，以跳过搜索空间中可能导致进一步冲突的部分。

Decision Making with a Reference Point.

DMRP is a new SAT solving approach that was proposed by Goldberg in [8,9]. Even though DMRP uses Boolean constraint propagation (BCP) with backtracking and learning from conflicting assignments it is not a simple variant of CDCL.译文：尽管DMRP使用布尔约束传播(BCP)来回溯并从冲突的赋值中学习，但它不是CDCL的一个简单变体。

In difference to CDCL solvers DMRP additionally holds a complete assignment (a so-called reference point).

译文：DMRP还持有一个完整的分配(一个所谓的参考点)

The algorithm aims for modifying the current reference point P to P’ in order to satisfy a clause under consideration. 译文：该算法的目的是将当前参考点P修改为P’，以满足考虑中的一个子句。

Furthermore, it is crucial that all clauses being satisfied by P remain satisfied by the modified reference point P‘ .

译文：此外，至关重要的是，所有被P所满足的子句都必须被修改的参考点P’所满足。

Algorithm 1 gives an overview of the DMRP approach, though this notation varies in some ways from the original notation in [9].译文：算法1概述了DMRP方法，尽管这种表示法在某些方面与[9]中的原始表示法不同。

One invocation of the DMRP subsolver (line 7 of Algorithm 1) takes a clause and a reference point as arguments.

译文：对DMRP子解算器(算法1的第7行)的一次调用采用子句和引用点作为参数。

It may either compute a modification to the reference point or it may learn the empty clause or else it times out.

译文：它可以计算对参考点的修改，或者学习空子句，或者超时。

The latter case causes the surrounding algorithm to call the DMRP subsolver with another unsatisfied clause.

译文：后一种情况会导致周围的算法调用带有另一个不满意子句的DMRP子解算器。

Some Adaptions for the Hybrid Approach

For the evaluation presented in this section we have run our solver for all industrial (application) instances of the SAT competitions resp. SAT Races of the years 2006 - 2009 that add up to 564 non-trivial4 instances. Each instance is preprocessed in advance and the timeout for the solvers was set to 1200 seconds. As a reference and also to check results we have run our CDCL solver using the Luby restart strategy (without DMRP) and MiniSAT 2.0 [6].

译文：每个实例都被预先预处理，并且求解器的超时设置为1200秒。作为参考和检查结果，我们使用Luby重启策略(没有DMRP)和MiniSAT 2.0运行了CDCL求解器

Figure 3 shows the results of different configurations of the hybrid approach. Furthermore, there are results that show performance of a pure DMRP solver. The presented configurations differ in the following issues that are related to decision making: As mentioned above the MakeCount may consider all clauses in D∪M (global) or only clauses in D (local). If two variables have the same MakeCount ties are broken in favour of the variable v that:

译文：图3显示了混合方法的不同配置的结果。译文：提出的配置在以下决策相关的问题上有所不同:

译文：如上所述，MakeCount可以考虑D∪M(全局)中的所有子句，也可以只考虑D(局部)中的子句；两个变量具有相同的MakeCount情况下，依照变量的下述属性区分：

(Act)      has the highest activity value similar to the VSIDS heuristic [18].

译文：(Act)  具有最高的活动值，类似于VSIDS启发式[18]

(BC)     has the smallest set R(v). This can be seen as a simple approximation of the BreakCount of the variable. In difference to the MakeCount the BreakCount of a variable v states the number of clauses that become unsatisfied by a flip of the value of variable v. 译文：这可以看作是对变量的BreakCount的简单近似。与MakeCount不同，变量v的BreakCount表示变量v的值翻转后不能满足的子句的数量。

(DC) was chosen least often for DMRP decisions. This avoids flipping always the same variables back and forth in different calls to solveDMRP. 译文：为DMRP决策选择最少的次数。这样就避免了在对solveDMRP的不同调用中总是来回翻转相同的变量。

The left plot of Figure 3 shows clearly that pure DMRP solving could not compete with CDCL solving. 译文：单纯的DMRP求解无法与CDCL求解相竞争。

Both pure DMRP configurations (global and local MakeCount) solve around 224 of 564 instances within 1200 seconds. Initial reference points are always chosen at random. Timeouts for the analysis of one reference point (one call to solveDMRP) are changed according to the Luby sequence. Modifying the strategy on how to choose initial reference points showed quite some impact. Our assumption was that DMRP requires a better guidance on where to start search and how to choose its initial reference points. That motivates our hybrid approach where DMRP gets its initial reference points indirectly from the CDCL solver. As the plots show this clearly improves the performance of the solver.

In this paper we have presented a data structure to implement the DMRP approach in an efficient way. Similar to the two-watched-literals scheme we choose one literal for each clause. The literal takes on responsibility so that a clause which is satisfied by a reference point is also satisfied by a modification of the point.

Moreover, we present a way how to determine that variable which satisfies the most previously unsatisfied clauses when its value is flipped (MakeCount). Based on this implementation we motivate a hybrid SAT solver that combines CDCL and DMRP solving.

Experiments have shown that our hybrid approach is competetive to the highly optimised state-of-the-art CDCL solvers and that the maintenance of complete assignments may definitely turn to account.

译文：在本文中，我们提出了一种数据结构来有效地实现DMRP方法。译文：与两种文字模式相似，我们为每个子句选择一个文字。译文：文字承担了责任，因此一个由参考点满足的子句也由该点的修改满足。

译文：此外，我们提出了一种方法来确定变量在其值被翻转时最满足之前未满足的子句(MakeCount)。译文：在此基础上，我们提出了一个结合CDCL和DMRP求解的混合SAT求解器。

译文：维持完成的赋值肯定会成为问题的关键。