非时序回溯与时序回溯代码分析(2023-9-1复习)

海阔凭鱼跃越 / 2023-09-01 / 原文

 

参考文献

[1] Alexander Nadel, Vadim Ryvchin:

Chronological Backtracking. SAT 2018: 111-121 

[2] Sibylle Möhle, Armin Biere:

Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting. GCAI 2019: 113-126 

[3] Hickey R., Bacchus F. (2020) Trail Saving on Backtrack. In: Pulina L., Seidl M. (eds) Theory and Applications of Satisfiability Testing – SAT 2020. SAT 2020. Lecture Notes in Computer Science, vol 12178. Springer, Cham. https://doi.org/10.1007/978-3-030-51825-7_4


 

求解器源码:Relaxed_LCMDCBDL_newTech

代码分析:

 

初始设置值:

    chrono, "Controls if to perform chrono backtrack", 100;
    conf_to_chrono, "Controls number of conflicts to perform chrono backtrack", 4000;

过程统计量:

    chrono_backtrack

    non_chrono_backtrack

   
 

search函数中关于非时序与时序的分支条件判断

// check chrono backtrack condition
if (   (confl_to_chrono < 0 || confl_to_chrono <= conflicts)     && chrono > -1    &&   (decisionLevel() - backtrack_level) >= chrono    )
{
++chrono_backtrack;
cancelUntil(data.nHighestLevel -1);
}
else // default behavior
{
++non_chrono_backtrack;
cancelUntil(backtrack_level);
}

解读:

(1)默认为非时序回溯;如果初始选项设置chrono为小于-1的值,则不会发生时序回溯;

(2)冲突数大于confl_to_chrono=4000,且chrono设置大于-1,则发生时序回溯主要取决于第三个条件回溯的层数跨度大于chrono=100;

可以看出,回溯跨度太大采用时序回溯可以提高求解性能。所谓“太大”选取100应该是一个实验得到的经验值。

 

   
 

 非时序回溯切换到时序回溯的原因分析文献中的表述:

可以看出,回溯跨度太大采用时序回溯可以提高求解性能。所谓“太大”选取100应该是一个实验得到的经验值。

   
 

 相关代码1:

//solver.h

 1 struct ConflictData
 2     {
 3         ConflictData() :
 4             nHighestLevel(-1),
 5             bOnlyOneLitFromHighest(false)
 6         {}
 7 
 8         int nHighestLevel;
 9         bool bOnlyOneLitFromHighest;
10     };

ConflictData FindConflictLevel(CRef cind);

 

 

//solver.cpp

 1 inline Solver::ConflictData Solver::FindConflictLevel(CRef cind)
 2 {
 3     ConflictData data;
 4     Clause& conflCls = ca[cind];
 5     data.nHighestLevel = level(var(conflCls[0]));
 6     if (data.nHighestLevel == decisionLevel() && level(var(conflCls[1])) == decisionLevel())
 7     {
 8         return data;
 9     }
10 
11     int highestId = 0;
12     data.bOnlyOneLitFromHighest = true;
13     // find the largest decision level in the clause
14     for (int nLitId = 1; nLitId < conflCls.size(); ++nLitId)
15     {
16         int nLevel = level(var(conflCls[nLitId]));
17         if (nLevel > data.nHighestLevel)
18         {
19             highestId = nLitId;
20             data.nHighestLevel = nLevel;
21             data.bOnlyOneLitFromHighest = true;
22         }
23         else if (nLevel == data.nHighestLevel && data.bOnlyOneLitFromHighest == true)
24         {
25             data.bOnlyOneLitFromHighest = false;
26         }
27     }
28 
29     if (highestId != 0)
30     {
31         std::swap(conflCls[0], conflCls[highestId]);
32         if (highestId > 1)
33         {
34             OccLists<Lit, vec<Watcher>, WatcherDeleted>& ws = conflCls.size() == 2 ? watches_bin : watches;
35             //ws.smudge(~conflCls[highestId]);
36             remove(ws[~conflCls[highestId]], Watcher(cind, conflCls[1]));
37             ws[~conflCls[0]].push(Watcher(cind, conflCls[1]));
38         }
39     }
40 
41     return data;
42 }

 

 1 //search函数中发生冲突代码段
 2 
 3 。。。
 4         ConflictData data = FindConflictLevel(confl);
 5         if (data.nHighestLevel == 0) {
 6             return l_False;
 7         }
 8 
 9         if (data.bOnlyOneLitFromHighest)
10         {
11             cancelUntil(data.nHighestLevel - 1);
12             continue;
13         }
14 
15         learnt_clause.clear();
16         if(DISTANCE) {
17             collectFirstUIP(confl);
18         }
19 
20         analyze(confl, learnt_clause, backtrack_level, lbd);
21         // check chrono backtrack condition
22         if (  (confl_to_chrono < 0 || confl_to_chrono <= conflicts) 
&& chrono > -1
&& (decisionLevel() - backtrack_level) >= chrono ) 23 { 24 ++chrono_backtrack; 25 cancelUntil(data.nHighestLevel -1); 26 } 27 else // default behavior 28 { 29 ++non_chrono_backtrack; 30 cancelUntil(backtrack_level); 31 } 32 33 lbd--; 34 。。。