基于加权平均值的一种分支启发式方法

摘要：

在可满足性(Satisfiability,SAT)问题算法中提出有效的分支策略可以提高求解器的效率,文中主要从冲突分析的角度出发,依据变量是否发生冲突和冲突的次数,提出一种基于加权平均值的分支启发式方法.该方法首先采用一组序列来记录变量是否参与冲突;其次赋予一个加权平均函数,依据变量的序列和决策层求出函数值;最后选择具有最大的函数值变量赋值,执行实例分析比较.由于该方法是对控制编码方法的改进,因此在进行例子分析时,采用了比较法和分析法,同时分析比较了所提方法、SUM(Sum in experiment)策略和ACIDS(Average Conflict-index Decision Score)策略.对SATLIB(SAT Little Information Bank)中的实例进行分析,结果表明所提方法能够实现更多子句被满足或最新冲突子句优先满足.

关键词：序列、加权平均、决策层、冲突次数、分支启发式

所属期刊栏目：45

分类号：TP181(自动化基础理论)

资助基金：国家自然科学基金项目:基于矛盾体分离的动态自动演绎推理研究61673320

在线出版日期：2018-12-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：117-120,131