基于分组的启发式SAT新算法——DC&DS算法  

Heuristic Boolean satisfiability algorithm based on grouping

作　　者：陈丽[1] 张必英[2] 

机构地区：[1]哈尔滨师范大学恒星学院数学与计算机系,哈尔滨150025 [2]哈尔滨商业大学计算机与信息工程学院,哈尔滨150025

出　　处：《计算机工程与应用》2008年第30期64-67,共4页Computer Engineering and Applications

基　　金：国家自然科学基金No.60273081~~

摘　　要：目前提高求解SAT问题完全算法的计算效率问题已成为挑战性研究问题。提出了一种基于启发式分组的SAT完备算法。启发式分组策略将一个全局搜索问题,转为局部搜索问题。并将该策略引入到结合BDD与SAT算法的形式验证中,与一般的启发式SAT算法相比,该算法在求解速度和求解问题的规模等方面都明显地改进了,实验结果表明了该算法的可行性和有效性。The paper gives the stl, dy of binary decision diagrams and Boolean satisfiability algorithms in formal verification method.It improves on Boolean satisfiability algorithms,and gives the DC＆DS algorithms.The paper gives equivalence checking algorithms in combinational circuit based on SAT,the arithmetic integrates the strongpoint of BDD and SAT,by restricting the size of constructing BDD,avoids EMS memory exploding.Reasoning minishes searching space of SAT.And apply this new algorithm in formal verification method based on BDD-SAT.Theoretical research and experimence results have proved the correctness of algorithms and design methods proposed in this paper.

关 键 词：形式验证 等价性验证 布尔可满足性 二叉判决图 

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