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