求解器器是参加2020求解器的简要说明

社区结构存在于现实问题之中，在形式化构成问题样例以后会发生显著变化，丢失部分社区特性。在有限的时间内充分利用社区特性是一个研究特点。此次参加竞赛的求解器，如同inIDGlucose求解器一样首先分析原始子句集文字的特征，并将其应用于求解器重启阶段首元素的选择上。基于现有的VSIDS及其变体，决策变元的选择策略延续到了重启首元素的选取上。在BCP过程中，决策变元的选择原则是一般情况是尽可能使用最近使用过变元这体现在一下两个方面：参与导出冲突的变元离冲突点近的变元的活跃度增量大于离冲突点远的变元；后期赋给变元的活跃度的增量要高于前期的（增量随冲突次数的增加除以一个小于1的衰减因子）。如果重启前求解器上一次运行期间已经陷入了局部空间，多次的反复回溯和传播会使得陷入局部的这部分变元的活跃度在全体变元中居于前列。此时的活跃度作为重启后决策变元的选择，可能就容易使得求解器不能实现真正意义上的重启。我们的指导思想是调整起步决策变元的选择方式，让重启的首变元从另外一种选择模式中产生。这样重启的首变元可能与已经陷入局部空间那部分便于所处的社区结构是不同。

由于社区结构的计算花费较长的时间，对与变元和子句较多的样例来说，求解社区结构的时间付出在参加竞赛的求解器中是不可接受的。虽然有很多求解器会在特殊时间段开展社区求解请加以利用，但都针对能满足较小社区求解时间的样例，尤其是当学习子句集也参与进来的情况。退而求其次，本次竞赛的版本中，将文字比较多的少数变元作为重启首变元备选变元；在重启时依次将备选变元之一作为重启首变元。同时，为了保证现有优良特性，以上改变决策变元的选择模式只用于少数重启阶段，并仅限于重启首变元的选取。

以上改变是在2019年冠军求解器的基础上修改的。除了以上我们自己的改进思想，也增加了2019年竞赛中新出现的有关极性选择新方法。

感谢。他们的求解器是我们学习和改进的基础。

设法限定求解时间，时期的变元基本出发点是，充分利用特性指导求解器  让一部分重启的首变元