论文部分内容阅读
解释布尔公式不可满足的原因在很多领域都具有实际的应用需求,而最小不可满足子式能够为诸如电路的自动综合等应用领域中的不可满足原因提供最精确的解释。因此,将两种能够高效求解最小不可满足子式的算法—分支-限界算法与贪心遗传算法,集成到解码电路的自动综合工具中。采用通信领域的标准编码电路作为测试集,将两种算法进行对比。实验结果表明，在运行时间与每秒剔除的短句数方面，贪心遗传算法优于分支-限界算法;不可满足子式在解码电路的自动综合过程中发挥重要作用。