【摘 要】
：
解释可满足性模理论(Satisfiability Modulo Theories,SMT)公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而极小不可满足子式能够为公式不可满足的原因提供
【机 构】
：
国防科技大学 计算机学院 湖南 长沙 410073
【出 处】
：
全国第15届计算机辅助设计与图形学学术会议
论文部分内容阅读
解释可满足性模理论(Satisfiability Modulo Theories,SMT)公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而极小不可满足子式能够为公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,准确诊断问题失败的本质缘由.本文针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其三类结点的概念,并证明了不可满足子式、极小不可满足子式与三类结点之间的映射关系。基于这种映射关系,采用宽度优先的搜索策略,提出了宽度优先搜索的极小SMT不可满足子式求解算法。基于业界公认的SMT Competition 2007测试集进行了实验,结果表明:该算法能够有效地求解极小不可满足子式.
其他文献
低功耗目前已成为嵌入式系统设计中非常重要的性能需求,动态电压调度(Dynamic Voltage Scaling,DVS)机制通过调整即时处理器电压进而有效降低系统功耗,正在逐渐得到广泛应用
依靠电池供电的嵌入式系统需要在整个设计过程中考虑功耗问题,但如何在系统级设计中进行低功耗软硬件划分还没有被充分研究.本文提出基于混沌神经网络的禁忌搜索算法解决嵌入
本文提出一种分层环状的NoC拓扑结构,该结构中链路具有两组环网,每组由一条数据环和一条控制环所组。针对于这种结构,提出了时分复用、优先级机制,空分路由分配,有保证服务策
我做次贷生意,专和银行谈判我的工作,就是帮那些还不起房贷的人和银行谈判,以低于房贷的价格,将房子卖掉。这样,银行虽然吃亏,但收回的是钱,而不是房子;贷款者获得解脱,保住
多线程技术是当前嵌入式系统开发中的常用技术,但一般都依赖于操作系统或者特定的函数库,通用性和可移植性较差.本文提出了一种通用的轻量级多线程模型1wThread,采用标准C语
本文描述了在层次式FPGA上的基于动态规划的布线算法策略.本文首先分析了层次式FPGA结构的特点,实现了基于树形的布线资源图动态规划的布线策略.它利用了层次式结构的特点,在
本文分析了用于高速串行收发系统接收端的时钟分频电路的设计,通过对扭环计数器计数原理的分析,提出了一种基于类扭环计数器的分频电路,该电路可以模式可选的实现奇数分频和
面对转基因食品,食用安全的问题是人们首先考虑的,例如插入基因的漂移、抗性、过敏和中毒等。众多专家对转基因食品的安全问题已经进行了许多研究,并在不少实际工作中得到应
针对参数化Cache一致性协议状态空间爆炸问题,本文提出共享集合伪临界值(pseudo-cutoff)的概念,有效优化了参数化目录Cache协议状态空间,并提出了解决小概率的大共享度事件的
存储设计是影响SoC系统性能和功耗的重要因素.在SoC系统级设计过程中,早期存储需求分析,有助于SoC设计与优化并缩短上市时间.本文提出一种面向SoC软硬件划分的多粒度应用程序