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

• 作者: 张必英 陈丽
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 形式验证 等价性验证 布尔可满足性 二叉判决图
• 年，卷（期）: 2008,（30）
• 所属期刊栏目: 理论研究
• 页码范围: 64-67
• 页数: 4页
• 分类号: TP301.6
• 字数: 4218字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2008.30.019

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈丽	哈尔滨师范大学恒星学院	4	6	2.0	2.0
2	张必英	哈尔滨商业大学计算机与信息工程学院	5	17	3.0	4.0