冲突发生时刻BCP蕴含关系图镜像给出很多信息。已经形成的功能和策略实施办法：
（1） 冲突分析得到学习子句；
（2） 参与冲突推导的变元活跃度的提升；
从最新的求解器代码分析，可以获取以下信息：
（1）参与冲突的各层变元、各层参与此次冲突的变元个数；
lichuming老师团队2018年关于DISTANCE方案中相关代码：
//solver.h声明数据成员和成员函数
bool collectFirstUIP(CRef confl);
vec<double> var_iLevel,var_iLevel_tmp;
uint64_t nbcollectfirstuip, nblearntclause, nbDoubleConflicts, nbTripleConflicts;
int uip1, uip2;
vec<int> pathCs;
CRef propagateLits(vec<Lit>& lits);
uint64_t previousStarts;
double var_iLevel_inc;
vec<Lit> involved_lits;
double my_var_decay;
bool DISTANCE;
|
|
1 //newVar（）函数中初始化相关数据成员 2 activity_distance.push(0);//新的变元活跃度数组
|
|
标签：变元,冲突,push,探究,蕴含,var,vec,iLevel From： https://www.cnblogs.com/yuweng1689/p/17679063.html