求解qbf问题的启发式调查传播算法

提出了一种启发式调查传播算法,并基于该算法设计了一种qbf(quantifiedbooleanformulae)求解器——hspqbf(heuristicsurveypropagationalgorithmforsolvingqbf)系统.它将surveypropagation信息传递方法应qbf求解问题中.利用surveypropagation作为启发式引导dpll(davis,putnam,logemannandloveland)算法,合适的变量进行分支,从而可以减小搜索空间,并减少算法回退的次数.在分支处理过程中,hspqbf系统结合元传播、冲突学习和满足蕴涵学习等一些优秀的qbf求解技术,从而能够提高qbf问题的求解效率.实验结明,hspqbf无论在随机问题上还是在qbf标准测试问题上都有很好的表现,验证了调查传播技术在qbf问解中的实际价值.