摘要：为了提高CDCL求解器的求解效率,针对可满足性(SAT)问题算法中决策变量的选择问题,提出了一种基于加权决策变量决策层的分支策略。这个新策略的主要思想是:基于布尔约束传播(BCP)过程中的回溯以及重启机制,首先考虑变量作为决策变量的次数以及所在决策层;其次,由于被选择的次数以及所在决策层不同,即占权重不同,对此进行加权;最后,结合冲突分析过程,对不同的变量给予不同的奖励得分。将不同变量在新策略与VSIDS和EVIDS策略中的得分进行对比,采用SATLIB(SAT Little Information Bank)中的大量例子进行实验测试,结果表明,新策略能够减少冲突次数以及求解时间(cpu),提高了求解器的求解效率。

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社