结合高级正向推理过程的可满足性问题解决器

【摘要】 提出了一个可满足性问题解决器,它结合了DPLL(Davis Putnam Loge-mann and Loveland)算法和作为高级推理技术之一的失败性文字检查(FLD,FailedLiteral Detection)技术.在失败性文字检查技术中,又提出了动态筛选方法,它包含了两条规则:内部和外部筛选.在保证能在每个决策层上发现大部分失败性文字的同时,降低了失败性文字检查所测试的文字数目及相应的计算时间.不同于其他类型的预定义的删除标准,在这一方法中文字的删除是动态的,从这点上讲,文中的失败性文字检查算法可以适应不同类型的测试基准实例.许多不必要的测试可以被避免,因而提高了失败性文字检查的计算速度.为了进一步提高失败性文字检查的效率,故此还增加了其他静态的测试约束.实验表明,经过优化后的失败性文字检查算法的效率明显高于其他的高级正向推理技术.更多还原