冲突发生时刻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);//新的变元活跃度数组
|
|