一种改进的有界模型检验子句规则

• 作者: 周晓方 周电 尹文波 荆明娥
• 来源期刊: 微电子学与计算机
• 关键词: 可满足性问题 有界模型检验 子句规则 精简布尔电路
• 年，卷（期）: 2007,（11）
• 页码范围: 103-106,109
• 页数: 5页
• 分类号: TN47
• 语种: 中文
• DOI: 10.3969/j.issn.1000-7180.2007.11.030

摘要

为有界模型检验提出了改进的子句规则.在节点分类的基础上,首先对精简布尔电路表示进行逻辑化简,去掉功能冗余节点;然后识别、记录和处理多元运算的操作数,把多元运算作为单个节点直接生成子句;最后合并相邻节点,根据合并后的逻辑关系生成变量和子句.实验结果表明,改进的子句规则普遍减少了可满足性问题的变量、子句数目和运行时间.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	荆明娥	复旦大学专用集成电路与系统国家重点实验室	13	57	4.0	7.0
2	尹文波	复旦大学专用集成电路与系统国家重点实验室	6	78	4.0	6.0
3	周晓方	复旦大学专用集成电路与系统国家重点实验室	52	292	10.0	13.0
4	周电	复旦大学专用集成电路与系统国家重点实验室	16	89	6.0	8.0