可满足性求解器中一种可观无关性利用方法

• 作者: 王昊 王秀芹 马光胜
• 来源期刊: 计算机辅助设计与图形学学报
• 学科: 工学
• 关键词: 可满足性 电路结构 可观无关性 控制唯一性
• 年，卷（期）: 2009,（2）
• 所属期刊栏目: VLSI设计与测试及电子设计自动化
• 页码范围: 183-189
• 页数: 7页
• 分类号: TP391.7
• 字数: 6857字
• 语种: 中文

摘要

为了提高可满足性求解器的效率,提出了一种利用电路可观无关性的方法.以带可观无关条件的CNF理论为基础,通过在可观无关条件计算时不使用变量排序,减少可观无关条件丢失.通过不对只出现在可观无关条件中的变量赋值,保证电路的控制唯一性.理论分析和实验结果表明,用该方法实现的可满足性求解器的搜索空间小、速度快.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	马光胜	哈尔滨工程大学计算机科学与技术学院	74	240	8.0	12.0
2	王昊	黑龙江科技学院计算机与信息工程学院	13	39	4.0	5.0
3	王秀芹	哈尔滨工程大学计算机科学与技术学院	2	5	1.0	2.0