基于高级正向推理技术的可满足性问题解决器研究

摘要

本文将高级正向推理技术之一的失败性文字检查技术(FLD,Failed Literal Detection)和DFLL(Davis Putnam Loge-mann and Loveland)算法相结合,提出了一个新型的可满足性问题解决器.该解决器采用两次失败性文字检查方法,首先应用对称扩展的一元推导实现对SAT问题的预处理,较深层次的发现失败性文字,并推导出更多的文字间的蕴含关系.再在预处理的结果上应用基于失败性文字检测的ACT筛选算法,在每个决策层上发现更多的失败性文字.实验表明该解决器不但使失败性文字检查效率得到提高,而且能够独立的解决一些实际问题和较难的SAT问题而无需进一步计算,充分的证明了该解决器具有对SAT问题有较强的处理能力.