As we know, the increment of EVSIDS is fixed whetherthe activity of variable is reached the critical value, i.e., theincrement is not concerned with conflict; it is concerned withthe period of conflict.譯文：我們知道，無論變數的活動是否達到臨界值，EVSIDS的增量都是固定的，即增量與衝突無關;它與衝突時期有關.

Different variables share the sameincrement in some cases. Intuitively, on the basis of the ruleof traversing binary tree, half of the rest of the searchingspace will be cut while any unassigned variable is assigned.

譯文：在某些情況下，不同的變數共享相同的增量。直觀地看，根據遍歷二叉樹的規則，當分配任何未分配的變數時，搜尋空間的一半將被切割。

Hence, we are forecasted boldly that the sequence ofassignments may have different influences on solving.

譯文：因此，我們大膽地預測，分配的順序可能會對求解產生不同的影響。

Thisis the motivation that we improve the branching algorithmand propose CRB. The CRB maintains a counter for eachvariable as EVSIDS, initialized to 0 at the beginning of thesearch. Whenever a variable is used in conflict analysis, thecounter is incremented by using the following equationwhere f is the damping factor given by EVSIDS.譯文：CRB為每個變數維護一個計數器作為EVSIDS，在搜尋開始時初始化為0。每當在衝突分析中使用一個變數時，計數器就會使用以下公式遞增，其中f是EVSIDS給出的阻尼因子。

W(v)is dynamic regulatory function that embodied the sequence of assignments.

This includes two aspects: decision levels and conflicts. LetnLevelsbe an integer variable that keeps the current decision levels,vLevelbe an integer variable that keeps thenLevelswhile the variable is assigned,nConflicts

nLevels當前決策級別的整型變數，vLevel分配變數時層級整型變數，

nConflicts是一個整型變數，記錄總的衝突數，vConflict是一個整型變數，在分配變數時保留nConflicts

\begin{equation*} W(v)=\alpha\cdot\frac{vLevel}{nLevels}+(1-\alpha)\cdot\frac{vConflict}{nConflicts}\ (0\leq\alpha\leq 1) \tag{2} \end{equation*}

Intuitively,W(v)approaches 1 while conflict derived by all of the unassigned variables at the current decision level.

The closer to the root levelvassigned, the smaller theW(v). Obviously,W(v)∈(0,1].

There have two differences between CRB and EVSIDS.

First, different variables (both decision variable and propagated variable) have different damping factors even led to same conflict.譯文：首先，不同的變數(包括決策變數和傳播變數)具有不同的阻尼因子，甚至會導致相同的衝突。

Second, the damping factor is smaller than EVSIDS of 1. Hence, the CRB slowed the growth rate in the overall.譯文：其次，阻尼因子小於EVSIDS的1。因此，CRB減緩了整體的增長率。

Large and sudden increases are the ones that tend to shorten the cycle time of entire damping and create frequent periodic damping.譯文：大而突然的增加往往會縮短整個阻尼的週期時間，併產生頻繁的週期性阻尼。

The CRB does not change the growth trends of score, i.e., variables which frequently led to conflict may have larger activity.譯文：CRB並沒有改變得分的增長趨勢，即經常導致衝突的變數可能具有更大的活動性。

--決策層----- 決策變數------決策之前對應的衝突數

35 x4 1001

36 x3 1120

37 x7 13695

38 x16 17367

By that analogy,W(x3)≈0.65+0.30⋅α,W(x7)≈0.79+0.19⋅α,W(x16)=α. Assume thatα=0.6, the CR of those variables are 0.79, 0.83, 0.90, and 1.00, respectively. Obviously the CR of decision variables from level 35 to 38 are nonlinear increased.Fig. 2illustrates the impact of different CR by different deceleration factors.

Fig. 3is a probability distribution image which illustrates how CRB is impact the searching process. The example instance is nameditox_ vc1130.cnfwhich from SAT-Race 2015. Here,αis 0.5. The total number of bumping is about 183403 and 152999 for EVSIDS and CRB respectively. As shown inFig. 3the CRB covers more domain of definition than EVSIDS, i.e., more variables can be updated to a smaller activity. The CRB maintains equal levels of quantity of variables which have stronger associations with conflict. This makes the branches more accurate and effective.

譯文：圖3是一個概率分佈圖像，說明了CRB是如何影響搜尋過程.

譯文：如圖3所示，CRB比EVSIDS覆蓋了更多的定義域，也就是說，可以將更多的變數更新為更小的活躍度。

譯文：CRB保持了與衝突有更強關聯的變數的相同數量水平。

譯文：這使得分支更加準確和有效。

In this section, we empirically compare the performance between the SAT solvers with different branching heuristics, EVSIDS and CRB, respectively.譯文：在本節中，我們根據經驗分別比較了具有不同分支啟發式的SAT求解器EVSIDS和CRB之間的效能。

Minisat[9]is a classical SAT solver with EVSIDS. Many state of the art SAT solvers are based on it. Since there are no more advanced heuristics in Minisat, it will enable us to better compare the efficiency of different branching heuristics.

For the original version of Minisat, we call it Minisat+EVSIDS. For fully evaluate the performance of CRB and further analyze the impact with decision level and conflict.

We have implemented 10 versions of CRB with different deceleration factors ofα. The modified solver only changed the branching heuristic by replacing EVSIDS with CRB. All of the default parameter settings and other features are left.譯文：我們實現了10個版本不同減速因子的CRB。改進的求解器只改變了分支啟發式，用CRB代替EVSIDS。所有預設引數設定和其他特性都將保留。

This comparison is made on the set of 300 instances from SAT Race 2015, each instance is limited to 3600s. The operating system is Hat Enterprise Red 6, with farm of Core(TM) i3-3240 3.4Ghz and 16G bytes physical memory.

Both Minisat+EVSIDS and Minisat+CRBs can run successfully without any preprocessors and all conclusions are correct.譯文：Minisat+EVSIDS和Minisat+CRBs都可以在不需要任何預處理的情況下成功執行，結論是正確的。

Table 1shows the Number of solved instances by original Minisat versus modified versions with CRB on SAT Race 2015 main track benchmarks. Minisat with EVSIDS solved 191 instances over the entire benchmarks, all of the modified versions with different deceleration factors solved more instances than Minisat.譯文：不同減速因子的改進版本求解的例項數都比Minisat多。

This illustrates CRB is more powerful than EVSIDS. In particular, the number of solved instances are growing linearly on the whole while0.1≤α≤1.0. It also shows the decision level has stronger influence than conflict number.譯文：這說明CRB比EVSIDS更強大。具體而言，在0.1≤1.0的情況下，解決例項的數量總體呈線性增長。決策水平的影響比衝突數量的影響更大。

The conference follows the Workshops on Satisfiability held in Siena
(1996), Paderborn (1998), and Renesse (2000), the Workshop on Theory
and Applications of Satisfiability Testing held in Boston (2001) and
in Cincinnati (2002). As in the last edition, the conference will host 
a SAT solver competition, and, starting from this year, also a QBF
solvers comparative evaluation. 

Great strides have been made in recent years in the theory and
practice of propositional satisfiability (SAT) testing.
譯文：近年來，命題滿足性(SAT)測試的理論和實踐取得了很大進展。
Even more recently, we have seen a growing interest in the theory and practice
of quantified Boolean formulas (QBFs 譯文：量化布林公式) satisfiability testing,witnessed 
by analogous advancements both on the theoretical and on the practical side. 
As a result there is growing interest in using SAT and QBF solvers 
as the basis for practical tools for solving real-world
problems, as well as using the insights gained from SAT and QBF
research to create problem-specific solutions.
譯文：因此，使用SAT和QBF解決器作為解決現實問題的實用工具的基礎，
以及使用從SAT和QBF研究中獲得的見解來建立具體問題的解決方案的興趣越來越大。

The purpose of this conference is to bring together researchers from
different communities -- including theoretical computer science,
artificial intelligence, verification, mathematical theorem-proving,
electrical engineering, and operations research -- in order to share
ideas and increase synergy(譯文：增加協同效應) between theoretical and empirical work.