摘要：提出一种基于随机方法和优化的dpll算法的测试用例自动生成技术,并以基于FPGA的核电仪控系统为对象进行了验证。该方法能验证HDL描述符合设计规范的要求,代码覆盖率较好,所提方法在解决大规模问题时效率有所提升,尤其是对于可满足性问题,效率提升非常显著。

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

摘要：在实际应用中通常需要求解对应CNF(Conjunctive Normal Form)公式之间仅相差几个子句的一系列SAT(Satisfiability Problem)问题,但目前绝大多数SAT求解算法都是针对单一SAT问题设计的。为此,基于dpll提出了ndpll算法,并在随机问题上对该算法的效率进行测试。实验结果表明,ndpll算法能一次性求解多个SAT问题,对于特定范围的CNF公式集具有较高的效率,CNF公式集的规模越大、相近因子越高、子句数和变量数的比值越大,则ndpll算法的效率越高。