基于趋势强度的SAT问题学习子句评估算法

针对命题逻辑公式求解过程中难以有效评估学习子句是否有利于后续搜索的问题,提出了一种基于学习子句趋势强度的评估算法。该算法首先通过分析学习子句在生存期内参与冲突分析的时间分布特征,将随机、离散的时间分布转换为连续的累积趋势强度；然后在删除周期达到时,通过设定趋势强度阈值删除在后续搜索过程中“不大可能”被使用的子句,保留“可能”被使用的子句；最后采用2015年、2016年SAT问题国际竞赛实例,将该算法与经典的活跃度评估算法和文字块距离(LBD)评估算法进行对比。实验结果表明,趋势强度评估算法在效率上明显优于活跃度评估算法,且求解的实例更多,同时与LBD算法基本持平。

Learnt Clause Evaluation Algorithm of SAT Problem Based on Trend Strength

For the problem that it is difficult to effectively evaluate whether the learnt clause is beneficial to the follo-wing search in the solving process of propositional logic equation,a clause evaluation algorithm was proposed based on the trend strength.First of all,the distribution characteristic of time involved in conflict analysis for the learnt clauses during the lifecycle is analyzed,and the random,discrete time distribution is transformed into the continuous cumulative trend strength.Then,when the deletion period arrives,the clauses with little possibility of being used in the subsequent search process will be deleted by setting the threshold of trend strength,while the clauses of high probability will be kept.Lastly,by using SAT international testing examples in 2015 and 2016,two state-of-the-art algorithms (i.e.,activi-ty evaluation algorithm and literal block distance (LBD) algorithm) are adopted for comparison purpose.The experimental results show that the proposed evaluation algorithm with trend strength can significantly outperform the activity evaluation algorithm in efficiency and can obtain more solving instances,and has the comparable performance with the LBD algorithm.