摘要
在可满足性(Satisfiability,SAT)问题算法中提出有效的分支策略可以提高求解器的效率,文中主要从冲突分析的角度出发,依据变量是否发生冲突和冲突的次数,提出一种基于加权平均值的分支启发式方法。该方法首先采用一组序列来记录变量是否参与冲突;其次赋予一个加权平均函数,依据变量的序列和决策层求出函数值;最后选择具有最大的函数值变量赋值,执行实例分析比较。由于该方法是对控制编码方法的改进,因此在进行例子分析时,采用了比较法和分析法,同时分析比较了所提方法、SUM(Sum in experiment)策略和ACIDS(Average Conflict-index Decision Score)策略。对SATLIB(SAT Little Information Bank)中的实例进行分析,结果表明所提方法能够实现更多子句被满足或最新冲突子句优先满足。
The effective branching strategy was proposed in the satisfiability(SAT)problem algorithm,which can improve the efficiency of the solver.In consideration of the conflict,according to whether the variables join in conflict and conflict times,a branching heuristic method based on added weight average value was proposed.Firstly,a sequence is used to record whether the variables are involved in the conflict.Secondly,a weighted average function is given,the function value is calculated through variable sequences and decision levels.Finally,variable with the largest value is assigned,example analysis and comparison are conducted.The new method is an improved method according to the control encoding method,so in the example analysis,the comparison and analysis ways were used,and SUM(Sum in experiment)strategy and ACIDS(Average Conflict-index Decision Score)strategy were compared with the new method at the same time.Through analysis of examples in SATLIB(SAT little information bank),the results show that more clauses are satisfied or the latest conflict clause can get the priority by the new method.
作者
胡忠雪
徐扬
胡容
HU Zhong-xue;XU Yang;HU Rong(School of Mathematics,Southwest Jiaotong University,Chengdu 610031,China)
出处
《计算机科学》
CSCD
北大核心
2018年第B11期117-120,131,共5页
Computer Science
基金
国家自然科学基金项目:基于矛盾体分离的动态自动演绎推理研究(61673320)资助
关键词
序列
加权平均
决策层
冲突次数
分支启发式
Sequence
Weighted average
Decision layer
Times of conflict
Branching heuristic
