非时序回溯与时序回溯代码分析(2023-9-1复习)
参考文献
[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; 过程统计量: chrono_backtrack non_chrono_backtrack |
|
search函数中关于非时序与时序的分支条件判断 // check chrono backtrack condition 解读: (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)
|
|