基于高级正向推理技术的可满足性问题解决器研究
本文将高级正向推理技术之一的失败性文字检查技术(FLD,Failed Literal Detection)和DFLL(Davis Putnam Loge-mann and Loveland)算法相结合,提出了一个新型的可满足性问题解决器.该解决器采用两次失败性文字检查方法,首先应用对称扩展的一元推导实现对SAT问题的预处理,较深层次的发现失败性文字,并推导出更多的文字间的蕴含关系.再在预处理的结果上应用基于失败性文字检测的ACT筛选算法,在每个决策层上发现更多的失败性文字.实验表明该解决器不但使失败性文字检查效率得到提高,而且能够独立的解决一些实际问题和较难的SAT问题而无需进一步计算,充分的证明了该解决器具有对SAT问题有较强的处理能力.
Propositional Satisfiability Problem Unit Propagation Implication Graph DPLL
王霄维 陈戈珩
长春工业大学计算机科学与工程学院 130012
国内会议
北京
中文
222-226
2009-10-01（万方平台首次上网日期，不代表论文的发表时间）