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

初始设置值：

    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应该是一个实验得到的经验值。