In this paper we introduce a more complex, but more efficient Early Conflict Detection BCP (ECDB) procedure that is able to achieve speedup by significantly reducing the total amount of work that the BCP procedure must perform.

我们介绍了一个更复杂但更有效的早期冲突检测BCP (ECDB)过程，它能够通过显著减少BCP过程必须执行的总工作量来实现加速。

A Chaff type solver starts by assigning a value to a literal based on a decision heuristic.

This literal is called the current decision literal. The solver then invokes the BCP procedure which detects all implications and conflicts associated with this decision.

Any implications that are found are added to the implication queue. This queue contains the consequences of assigning the current decision literal to its current value.

Implications in this queue can also trigger other implications.

The BCP procedure must process all these implications before the solver is free to make another decision.

If in the process of evaluating this queue it runs into a conflict, in which two clauses force a single literal to opposite values, a conflict signal is generated.

A conflict analysis procedure is then invoked to find the reason and the origin of the conflict. Based on this information, the assignment stack (chronologically ordered list of all defined literals) is corrected to resolve the conflict.

The BCP procedure is then rerun to check the implications of this correction.

The decision-making, BCP, and conflict analysis procedures continue until either a solution is found or the problem is proven unsatisfiable.

When evaluating clauses during the BCP stage, the implication queue can become quite large (100’s of entries in the queue are normal).

The larger it becomes, the more information about the current problem it contains; and the better the probability of a conflict existing within the queue.译文：蕴含文字队列变得越大，它包含的关于当前问题的信息就越多;并且队列中存在冲突的概率越高。

The idea behind the ECDB procedure is to utilize this information to generate unit clauses and subsequently conflict clauses sooner.

An example of how this is done will be shown in section 4.

Secondly, the implication queue can be used to better evaluate clauses.

译文：其次，可以使用隐含队列更好地评价子句。

This better evaluation of clauses leads to better choices for watched literals, reducing the chance that a clause needs to be reevaluated in the future. This better utilization of the implication queue is the major improvement when compared to other solvers.

MIRA was created because Full ECDB could not be efficiently implemented in Chaff.

MIRA is still based on Chaff inheriting such features as conflict analysis and fast BCP using watched literals.

MIRA, however, gains considerable speedup over Chaff through the use of a new ECDB procedure that has three modes of operation: Full ECDB; Partial ECDB; and No ECDB.

Note that all three versions of MIRA share the same Decision, Conflict Analysis, and Clause Management procedures.

3.1 No ECDB

The No ECDB mode contains no improvements to detect conflicts early. This makes it more like a Chaff type solver for comparison.

The first improvement of the Partial ECDB mode when compared to Chaff is how unit clauses are handled.

译文：与Chaff相比，部分ECDB模式的第一个改进是单元子句的处理方式。

Given an implication queue, Chaff would examine all entries in chronological order ignoring conflicting implications (e.g. two separate clauses that force a single literal but to opposite values).

Before Chaff detects this conflict, it must process the entire implication queue up until the point where the first of the conflicting implications is located (assuming no other conflicts exist).译文：在Chaff检测到这个冲突之前，它必须处理整个隐含队列，直到第一个冲突隐含所在的位置(假设不存在其他冲突)。

The implication queue can be quite large, forcing Chaff’s BCP procedure to process many clauses that are not required.译文：与箔条相比，部分ECDB模式的第一个改进是单元子句的处理方式。

MIRA in contrast, checks the implication queue for conflicts before adding implications.译文：在添加蕴含之前检查蕴含队列是否有冲突。

If a conflict exists, the conflict resolution procedure is immediately invoked. This is similar to what is done in Limmat [10].

This partial version also goes beyond Limmat allowing for fast clause evaluation when the other watched literal is correctly defined, even if that literal is in the implication queue and has not yet been processed by the BCP procedure.

译文：这个部分版本还超越了Limmat，允许在其他观察的文字正确定义时快速计算子句，即使该文字在隐含队列中，还没有被BCP过程处理。

This is done as the implication queue and assignment stack are already available together because of the full ECDB part of MIRA. 

译文：这是因为MIRA的完整ECDB部分使得隐含队列和赋值堆栈已经可用。

This also allows for a better utilization of the data structure MIRA uses to store clauses.译文：这还允许更好地利用MIRA用于存储子句的数据结构。

Note that when MIRA is in Partial ECDB mode the clause data structure is the same as the one presented in Figure 1 below, however the CV variable is not used. 译文：注意，当MIRA处于Partial ECDB模式时，子句数据结构与下面图1中所示相同，但是没有使用CV变量。

The data structure is therefore similar to the one presented in [9] where the authors compared different WL schemes. 译文：因此，数据结构与[9]中作者比较了不同的WL方案的数据结构相似。

The Full ECDB mode of MIRA goes even further.

Here, the ECDB procedure is still similar to Chaff when it traverses the watched literal list of the current decision variable.

However, unlike Chaff which checks literals in the order that they were added to the implication queue, MIRA first checks the implications that are most likely to cause a conflict. 

译文：然而，不像Chaff按照字面量被添加到含义队列的顺序检查，MIRA首先检查最有可能引起冲突的含义。

The heuristic for this is described in section 6.

Secondly, once a literal has been added to the implication queue, it becomes immediately defined throughout the entire BCP procedure. 译文：一旦一个字面值被添加到隐含队列中，它就会立即在整个BCP过程中被定义。

Consequently, the BCP procedure uses both the assignment stack and implication queue when evaluating a particular clause for a free or properly assigned literal (a literal assignment that satisfies the clause).

译文：BCP过程使用赋值堆栈和隐含队列对特定子句求值以获得空闲或正确赋值的文字(满足子句的文字赋值)。

This ensures that it does not choose a new watched literal that is improperly assigned in the implication queue and thus reduces the probability that the clause will be re-evaluated.

译文：这确保了它不会选择一个在隐含队列中分配不当的新的被监视的文字，从而降低了子句被重新计算的可能性。

Moreover, evaluating clauses in this manner allows the BCP procedure to generate unit and conflict clauses sooner.译文：此外，以这种方式评估条款允许BCP程序更快地生成单元和冲突条款。

An example of how powerful Early Conflict Detection is will be discussed below in section 4. Also, since Chaff’s conflict analysis procedure as is cannot handle re-ordered assignment stacks, MIRA’s procedure will be discussed in section 7.

Using the sample CNF from section 2 for this example, Chaff would start by assigning x1 = 1.

It would then check all the clauses (assuming Chaff is currently watching the first two literals of every clause).

While checking the clauses it would find the unit clause (?x1 + x2) and assign x2 = 1 in the implication queue.

Once done checking all the clauses in the watched literal list for x1 = 1, it would then move onto the next literal in the implication queue, forcing x2 = 1.

It must then look at clauses that contain ?x2 as a watched literal (in this case the last two clauses).

Again, while going through the clauses it could find two more unit clauses and it would add x3 to the implication queue.

Partial ECDB would find the conflict here as two clauses force x3 to opposite values.

Chaff though, would continue with x2 = 1 until all clauses are checked. Then it would check clauses for x3, and only then will it find the conflict.

In Full ECDB mode, the conflict is generated on the first pass. If x1 = 1 is the first decision the ECDB procedure will immediately add x2 = 1 to the assignment stack as soon as it evaluates the first clause.

The ECDB procedure will then evaluate the second clause. It will see that since x1 = 1 and x2 = 1, x3 = 1 is the only possible solution (unit clause).

Again it will add x3 = 1 to the assignment stack. Then, when it evaluates the third clause a conflict will be immediately generated.

By utilizing more of the information available at each step of the ECDB procedure, the unit clause stack grows faster than Chaff’s, producing unit clauses faster, and then either arriving at an answer or a conflict sooner.

译文：通过在ECDB过程的每个步骤中利用更多的可用信息，单元子句堆栈比Chaff的增长更快，产生单元子句更快，然后要么更快地得到答案，要么更快地产生冲突。

This significantly reduces the number of clauses the BCP procedure evaluates. 译文：这大大减少了BCP过程计算的子句数量。

Also, by allowing the BCP procedure to make better choices when exchanging the watched literals, it can further reduce future BCP operations. 译文：此外，通过允许BCP过程在交换被监视的字面量时做出更好的选择，它可以进一步减少未来的BCP操作。

An example of this is when Chaff evaluates a clause, it might replace the current watched literal with a literal that is wrongly assigned in the implication queue.译文：举个例子，当Chaff计算一个子句时，它可能会用一个在隐含队列中错误分配的字面值替换当前监视的字面值。

In this way MIRA avoids the future re-evaluation of the clause that Chaff would be required to do.译文：通过这种方式，MIRA避免了Chaff将来需要做的对条款的重新评估。

The BCP procedure of any SAT Solver normally represents over 80% of the processing time [2], so it is crucial that it is efficiently implemented.

To optimize the BCP procedure in MIRA, the implication queue was combined with the assignment stack.

A separate Literal Value Array (LVA) was created for the BCP procedure when evaluating clauses.

The LVA contains the value for all literals that are defined (decisions and implications). This allows the ECDB to easily check clauses as it only uses the one array.

If it finds a unit clause, it must update both the assignment stack and the LVA.

The same is true when backtracking. Lastly, there is a pointer that points to the end of the assignment stack and another that points to the current position of the ECDB procedure within this stack.

The second pointer is required because the ECDB procedure must still check all implications that are associated with the current decision to ensure correctness. In this way all clauses that are in each decision’s or implication’s watched literal clause list are eventually checked if no conflict is found.

Note that this stack will routinely be re-ordered to ensure the best implications are checked first and the heuristic for this is described in section 6.

译文：请注意，这个堆栈将例行地重新排序，以确保首先检查最佳含义，关于这一点的启发式描述在第6节。

The ECDB procedure also arranges clauses into a special data structure that allows it to work efficiently.译文：ECDB过程还将子句安排到一个特殊的数据结构中，使其能够有效地工作。

In Chaff’s watched literal scheme the pointers for the watched literals float, meaning their position in the clause is not fixed. 译文：在Chaff的观察字面值模式中，观察字面值的指针是浮动的，这意味着它们在子句中的位置不是固定的。

This is nice when replacing watched literals because no literal swapping is required, however because of this, Chaff does not know the exact position of the both watched literals within a clause.译文：这在替换被监视的字面值时很好，因为不需要进行字面值交换，然而正因为如此，Chaff并不知道两个被监视的字面值在子句中的确切位置。

In MIRA, each clause follows the data structure in Figure 1. In the diagram WL0 and WL1 are the two watched literals of that clause. The watched literals of a clause are always located in the first two positions.

This structure is similar to the one presented in [10] but contains the CV variable which is an important modification and will be discussed later.

This structure is used in all three ECDB versions of MIRA and allows the ECDB procedure to easily check the value of the other watched literal. 译文：这个结构在MIRA的所有三个ECDB版本中都使用，并允许ECDB过程轻松地检查其他被监视文字的值。

The other or second watched literal can have three possible values: properly defined; undefined; or improperly defined. 译文：另一个或第二个监视的文字可以有三个可能的值:正确定义;未定义的;或不正确的定义

If the second watched literal is properly defined, which on the benchmarks shown in section 9 is on average about 60% of the time, the ECDB procedure can move onto the next clause without evaluating the rest of the current clause.

译文：如果第二个被观察的文字被正确定义(在第9节所示的基准测试中，它的平均时间约为60%)，ECDB过程可以转移到下一个子句，而不需要计算当前子句的其余部分。

This results in a significant increase in BCP clause throughput (the number of clauses checked by the BCP procedure in a set period of time).

For this very reason and to further improve the chance that it does not need to evaluate the entire clause, the Partial ECDB version incorporates the implication queue when examining the other watched literal. 译文：出于这个原因，并为了进一步提高不需要计算整个子句的可能性，Partial ECDB版本在检查其他被监视的文字时合并了含义队列。

Also, since both watched literals are in sequential memory addresses, it is likely that they are both loaded into the same cache line. This reduces accesses to main memory, increasing the effectiveness of the cache. 译文：而且，由于两个被监视的字面值都在顺序内存地址中，所以很可能它们都被加载到同一高速缓存线中。这减少了对主存的访问，增加了缓存的有效性。

In the second most common case, where the other watched literal is undefined, the procedure is the same as Chaff’s, and MIRA looks for a new literal to replace the current one. 译文：在第二种最常见的情况下，另一个被监视的文字是未定义的，这个过程与Chaff的过程相同，MIRA寻找一个新的文字来替换当前的文字。

If this fails, a unit clause is reported and a variable is added to the implication queue. 译文：如果失败，则报告一个单元子句，并向隐含队列添加一个变量。

When using the Full ECDB procedure there is also a third and more complicated case when the second watched literal is incorrectly defined.译文：在使用Full ECDB过程时，还有第三种更复杂的情况，即第二个观察的文字定义不正确。

In Chaff, this case would constitute a conflict, but in MIRA implications can be defined but not yet processed. 译文：在Chaff中，这种情况将构成冲突，但在MIRA中可以定义影响，但尚未处理。

This means that Full ECDB procedure does not immediately know if the current clause is a conflicting clause and it must therefor search the clause for a free or properly defined literal. 译文：这意味着Full ECDB过程不能立即知道当前子句是否是冲突子句，因此它必须在子句中搜索*的或正确定义的文字。

If during the search a free or properly defined literal is not found, a conflict will be signalled and the conflict resolution procedure will be run. 译文：如果在搜索过程中没有找到*的或正确定义的文字，则会发出冲突信号，并运行冲突解决过程。

However, if a free or properly defined literal is found, MIRA will replace the current WL with it. The algorithm will then continue searching the clause for a second undefined or properly defined literal.

译文：但是，如果找到一个*的或正确定义的文字，MIRA将用它替换当前的WL。然后，算法将继续在子句中搜索第二个未定义或正确定义的字面值。

If it does not find one then the current clause is a unit clause and MIRA will define the literal that needs to be defined. However, if MIRA finds another free literal, it will be swapped with the cache variable (called the CV, and is the third variable in a clause) and not with the other watched literal.

译文：如果没有找到，那么当前子句就是一个单元子句，MIRA将定义需要定义的文字。然而，如果MIRA找到了另一个*字元，它将与缓存变量(称为CV，是子句中的第三个变量)交换，而不是与其他被监视的字元交换。

This is because it is difficult for MIRA to find (and then remove) the reference to the current clause from the other watched literal’s clause list (the list of all clauses that have this literal as a watched literal). 译文：这是因为MIRA很难从另一个受监视字面量的子句列表(所有将该字面量作为受监视字面量的子句列表)中找到(然后删除)对当前子句的引用。

The CV is there to reduce the future work the BCP must do when it tries to replace the other watched literal, as there is a good chance the third literal is free or properly defined. 译文：CV的存在是为了减少BCP在试图替换其他被监视的文字时必须做的工作，因为第三个文字很有可能是*的或正确定义的。

This avoids researching the entire clause. 译文：这样可以避免研究整个子句。

The use of the CV further reduces the effect of the second search because of its physical location which is normally on the same cache line as the watched literals. 译文：使用CV进一步降低了第二次搜索的效果，因为它的物理位置通常与所观察的文字在同一高速缓存线上。

This further increases the cache friendliness as each clause has a relatively small effective cache foot print. 译文：这进一步增加了缓存友好性，因为每个子句的有效缓存占用空间相对较小。