计算机工程与应用 ›› 2008, Vol. 44 ›› Issue (30): 64-67.DOI: 10.3778/j.issn.1002-8331.2008.30.019

• 理论研究 • 上一篇    下一篇

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

陈 丽1,张必英2   

  1. 1.哈尔滨师范大学 恒星学院 数学与计算机系,哈尔滨 150025
    2.哈尔滨商业大学 计算机与信息工程学院,哈尔滨 150025
  • 收稿日期:2007-11-28 修回日期:2008-02-20 出版日期:2008-10-21 发布日期:2008-10-21
  • 通讯作者: 陈 丽

Heuristic Boolean satisfiability algorithm based on grouping

CHEN Li1,ZHANG Bi-ying2   

  1. 1.Departement of Mathematics and Computer Science,Star College,Harbin Normal University,Harbin 150025,China
    2.Computer and Information Engineering College,Harbin University of Commerce,Harbin 150025,China
  • Received:2007-11-28 Revised:2008-02-20 Online:2008-10-21 Published:2008-10-21
  • Contact: CHEN Li

摘要: 目前提高求解SAT问题完全算法的计算效率问题已成为挑战性研究问题。提出了一种基于启发式分组的SAT完备算法。启发式分组策略将一个全局搜索问题,转为局部搜索问题。并将该策略引入到结合BDD与SAT算法的形式验证中,与一般的启发式SAT算法相比,该算法在求解速度和求解问题的规模等方面都明显地改进了,实验结果表明了该算法的可行性和有效性。

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

Abstract: The paper gives the study 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.

Key words: formal verification, simulation, Boolean satisfiability, binary decision diagrams