欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
为有界模型检验提出了改进的子句规则。在节点分类的基础上。首先对精简布尔电路表示进行逻辑化简，去掉功能冗余节点；然后识别、记录和处理多元运算的操作数，把多元运算作为单个节点直接生成子句；最后合并相邻节点，根据合并后的逻辑关系生成变量和子句。实验结果表明，改进的子句规则普遍减少了可满足性问题的变量、子句数目和运行时间。
英文摘要：
A new Clause Form for Bounded Model Checking is proposed. First, RBCs nodes are divided into two classes, Second, logic simplifying is performed to remove node with functional redundancy. Then muhi-operands operation is considered to be a single node to produce CNF clauses directly. In the end, the method of merging adjacent logical nodes is used to produce minimal CNF variables and clauses. The efficiency of the proposed approach is shown through its application on benchmark circuits.
同期刊论文项目
同项目期刊论文
期刊信息
位置：