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

作　　者：荆明娥[1] 周电[1] 唐璞山[1] 周晓方[1] 张华 

机构地区：[1]复旦大学微电子研究院专用集成电路国家重点实验室,上海201203 [2]Department of Electrical Engineering The University of Texas at Dallas

出　　处：《中国科学（E辑）》2007年第12期1597-1606,共10页Science in China(Series E)

基　　金：中国国家自然科学基金(批准号:60773125;90207002;90307017;60676018);美国国家科学基金(CCR-0306298);中国博士后科学基金(批准号:KLH1202005);上海市自然科学基金(批准号:06ZR14016)资助项目

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

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

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构] O225[自动化与计算机技术—计算机科学与技术]