标签：out after 计算 sign fflush 活跃 its ror current
变元活跃度计算模式有：VSIDS、基于历史出现时刻与当前冲突时刻距离等
有三个最小堆：
// A priority queue of variables ordered with respect to the variable activity.
Heap<VarOrderLt> order_heap_CHB,
order_heap_VSIDS,
order_heap_distance;
一般的求解切换方式是：
conflicts < 10000 采用 VSIDS
之后 采用CHB 直至求解器运行2500s
随后回复采用VSIDS
具体代码在solve_函数前部设置触发函数，函数内设置触发器实现按指定求解时间进行模式切换。
1 //static bool switch_mode = false; 2 //static void SIGALRM_switch(int signum) { switch_mode = true; } 3 4 // NOTE: assumptions passed in member-variable ‘assumptions‘. 5 lbool Solver::solve_() 6 { 7 signal(SIGALRM, SIGALRM_switch); 8 alarm(2500); 9 。。。 10 f (!VSIDS && switch_mode){ 11 VSIDS = true; 12 printf("c Switched to VSIDS.\n"); 13 fflush(stdout); 14 picked.clear(); 15 conflicted.clear(); 16 almost_conflicted.clear(); 17 #ifdef ANTI_EXPLORATION 18 canceled.clear(); 19 #endif 20 }
。。。
Since the solver M APLE SAT [5], the decision heuristic is
switched back from the currently selected one to VSIDS –
after 2500 seconds. As solver execution does not correlate
with run time, this decision results in solver runs not being
reproducible. To fix this property, the switch to VSIDS is now
dependent on the number of performed propagations as well
as conflicts. Once, one of the two hits a predefined limit,
the heuristic is switched back to VSIDS. This change enables
reproducibility and deterministic behavior again.
在切换第三阶段，基于固定冲突次数切换恢复采用 VSIDS可以使得求解过程和结果具有重现。
具体做法如下：
（1）在solver.h文件中声明三个量
1 int64_t VSIDS_conflicts; // conflicts after which we want to switch back to VSIDS 2 int64_t VSIDS_propagations; // propagated literals after which we want to switch back to VSIDS 3 bool reactivate_VSIDS; // indicate whether we change the decision heuristic back to VSIDS
（2）在solver.cc文件中
构造函数中初始化三个变量的值如下：
1 , VSIDS_conflicts(120000000) 2 , VSIDS_propagations(3000000000) 3 , reactivate_VSIDS(false)
随后在函数solve_中切换代买段改为：
1 //-------------------------------------------------------------- 2 // switch back to VSIDS? 3 if (!reactivate_VSIDS && ((VSIDS_conflicts > 0 && VSIDS_conflicts < conflicts) || 4 (VSIDS_propagations > 0 && VSIDS_propagations < propagations))) 5 reactivate_VSIDS = true; 6 //-------------------------------------------------------------- 7 if (!VSIDS && reactivate_VSIDS){ 8 VSIDS = true; 9 printf("c Switched to VSIDS.\n"); 10 fflush(stdout); 11 picked.clear(); 12 conflicted.clear(); 13 almost_conflicted.clear(); 14 #ifdef ANTI_EXPLORATION 15 canceled.clear(); 16 #endif 17 }
标签：out after 计算 sign fflush 活跃 its ror current
原文地址：https://www.cnblogs.com/yuweng1689/p/12617028.html
