启发式极性决策算法解SAT问题

摘要：

提出了一种启发式极性决策的可满足性问题(SAT)新算法. 该算法继承了当前SAT解决器的许多策略: 快速BCP、子句记录、重启动搜索等. 同时, 该算法通过预先根据Karnaugh图的覆盖分布计算变量极性, 将其加入到DPLL的决策过程中, 大大降低了搜索过程中的冲突次数. 实验表明采用该算法的解决器--DiffSat, 能够解决许多目前最有效的解决器Zchaff和MiniSat所不能解决的实例. 尤其是对于Bart基准系列中的每个实例, DiffSat都能够在0.03 s内解决, 而Zchaff和MiniSat在给定的900 s内不能够解决大部分实例. 而且, DiffSat解决器在某些实例上的特性远远优于具有代表性的基于不完全随机算法的解决器DLM.

关键词：可满足性问题、DPLL、完全算法、变量决策

所属期刊栏目：37

分类号：TP3(计算技术、计算机技术)

资助基金：国家自然科学基金60773125;90207002;90307017;60676018;美国国家科学基金CCR-0306298;中国博士后科学基金KLH1202005;上海市自然科学基金06ZR14016

在线出版日期：2008-04-09（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：1597-1606