非时序回溯与时序回溯代码分析2（2023-9-7）-526互联

采用CB+NCB的方式后传播序列trail各层中的文字层序属性发生了变化，原有层数的递增、同层文字属于单一层序发生了变化。

[1] Alexander Nadel, Vadim Ryvchin:Chronological Backtracking. SAT 2018: 111-121

In particular, the decision level of the variables in the assignment trail is no longer monotonously increasing.

赋值轨迹中变量的决策水平不再单调递增。

涉及决策水平不在单调递增的相关函数及其代码段如下：

//传播函数后半段代码

 1 CRef Solver::propagate()
 2 {
 3    。。。
 4            if (value(first) == l_False){
 5                 confl = cr;
 6 
 7                 //--------------------------------------------------------
 8                 conflTrailIndex = qhead -1;  //记录冲突点索引
 9                 if( conflTrailIndex == trail_lim[trail_lim.size() - 1] )
10                 {
11                     confLitIsDecLit_Tag = 1;
12                 }                                           
13                 //--------------------------------------------------------
14 
15                 qhead = trail.size();
16                 // Copy the remaining watches:
17                 while (i < end)
18                     *j++ = *i++;
19             }else
20             {
21                 if (currLevel == decisionLevel())
22                 {
23                     uncheckedEnqueue(first, currLevel, cr);
24 #ifdef PRINT_OUT                    
25                     std::cout << "i " << first << " l " << currLevel << "\n";
26 #endif                    
27                 }
28                 else
29                 {
30                     int nMaxLevel = currLevel;
31                     int nMaxInd = 1;
32                     // pass over all the literals in the clause and find the one 
                          with the biggest level
33                     for (int nInd = 2; nInd < c.size(); ++nInd)
34                     {
35                         int nLevel = level(var(c[nInd]));
36                         if (nLevel > nMaxLevel)
37                         {
38                             nMaxLevel = nLevel;
39                             nMaxInd = nInd;
40                         }
41                     }
42 
43                     if (nMaxInd != 1)
44                     {
45                         std::swap(c[1], c[nMaxInd]);
46                         *j--; // undo last watch
47                         watches[~c[1]].push(w);
48                     }
49                     
50                     uncheckedEnqueue(first, nMaxLevel, cr);
51 #ifdef PRINT_OUT                    
52                     std::cout << "i " << first << " l " << nMaxLevel << "\n";
53 #endif    
54                 }
55             }
    。。。