论文部分内容阅读
针对目前大部分可满足性(SAT)问题算法中变量选择问题,提出一种基于短子句的分支策略。这个新思想的主要方法是:首先,赋予每个变量一个权重,依据变量的得分值来进行赋值;其次,在进行布尔约束传播过程时发生冲突后,依据对新产生的学习子句中变量所在决策层和冲突层的平均值的大小条件来对其增加得分,未参与冲突的变量分值保持不变;最后,选择得分最高的变量并赋值,重新进行布尔约束传播。分析结果表明,与变量状态独立衰减分值(VSIDS)策略相比,所提出新策略决策次数和平均运算时间较少,运算效率较高。新的策略优先满足短