摘要：随着软硬件设计规模日益增加,功能越来越复杂,功能验证与调试在整个设计周期中占有的比重越来越大,迫切需要高效的方法诊断与定位设计中的错误,而求解不可满足子式可以显著提高自动化工具定位错误的效率.近年来,求解不可满足子式的算法多是基于DPLL(Davis-Putnam-Logemann-Loveland)回溯搜索过程的完全算法,很少有研究涉及到不完全方法.文中针对求解不可满足子式的不完全方法,提出了悖论证明与悖论解析树的概念,并提出一种启发式局部搜索算法,从布尔公式的悖论证明中求解不可满足子式.算法首先采用融合了布尔推理技术、动态剪枝方法及蕴含消除方法的局部搜索过程,逐步构建悖论证明所对应的悖论解析树;然后调用递归函数搜索悖论解析树,最终得到不可满足子式.基于实际测试集与随机测试集进行了实验对比,结果表明文中提出的算法优于同类算法,而且动态剪枝与蕴含消除技术能够有效地减少存储空间及运行时间.

摘要：解释布尔公式不可满足的原因在诸如形式化验证与电子设计自动化等众多领域中都具有非常重要的理论与应用价值.不可满足子式能够为布尔公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由.针对近年来出现的许多求解布尔不可满足子式的研究工作,根据算法的类型归类比较,对各种求解方法进行了概述评论,并简要介绍了在该领域所做的一些研究工作.最后讨论了布尔不可满足子式的求解方法目前面临的主要挑战,并对今后的研究方向进行了展望.

摘要：随着VLSI(Very Large Scale Integrated)芯片设计的规模越来越大,功能越来越复杂,在FPGA(Field Programmable Gate Array)上实现或进行原型验证时,往往会出现布线拥塞或无法布通的情况.而不可满足子式能够迅速诊断FPGA无法布通的原因,并且精确定位关键线网.针对如何加速FPGA详细布线过程,提出了一种基于消解否证的启发式局部搜索算法,能够快速从布尔公式中提取不可满足子式.基于典型的FPGA布线测试集,与两种求解最小不可满足子式效率最高的算法进行了比较,结果表明局部搜索算法在运行效率方面显著优于分支限界算法与贪心遗传算法,而局部搜索算法也能得到最小不可满足子式;并且深入分析了不可满足子式在FPGA详细布线中的作用,能够加速芯片的设计与验证过程.

摘要：为了广泛有效地将不可满足子式应用于知识验证、产品规划、硬件和软件的设计与验证等领域,对不可满足子式进行了相关研究.对当前不可满足子式的主要相关算法进行了概述评论、分类归纳,并从计算复杂性角度介绍了其子类、参数复杂性以及QBF中的极小不可满足子式.总结了近10年来不可满足子式的理论与算法,讨论了不可满足子式的未来研究发展方向.研究有利于进一步发现不可满足的根本原因,从而进行有针对性地改进,并对相关人员的研究提供帮助.

摘要：求解布尔不可满足子式在超大规模集成电路设计与验证领域都具有非常重要的理论与应用价值,帮助EDA工具迅速定位错误与不一致。针对求解不可满足子式的非完全方法,提出了消解悖论与悖论解析树的概念,在此基础上提出一种启发式局部搜索算法。该算法根据公式的消解规则,采用局部搜索过程直接构造证明不可满足性的悖论解析树,而后递归搜索得到不可满足子式;算法中融合了布尔推理技术、动态剪枝方法及蕴含消除方法以提高搜索效率。基于随机测试集进行了实验对比,结果表明提出的算法优于同类算法。