SMT求解器增强技术的研究

摘要

在计算机集成电路不断飞速发展的信息时代，无论计算机的硬件还是软件设计的复杂度都在不断提高，也对开发设计提出了新的挑战，尤其是在保证新产品的安全性、可靠性和正确性方面。为了解决该难题，将计算机辅助设计概念引入测试、验证等领域逐渐形成了新的技术发展趋势。而可满足性问题，包括SAT和SMT两方面已经成为最近10年中的研究热点。与其相关的技术都在不断发展中得到了性能的提高和功能的完善。在发展的同时SMT求解器可在许多新的领域得到了应用，优化问题则是其中的重要的领域。因此，本文就可满足性求解技术的增强以及该种技术与优化问题如何结合等问题做了如下研究：
　　 1．研究已有的冲突分析算法，设计新的冲突分析和学习算法。该种算法旨在使用尽量少的冲突节点，产生出更为有效且更加简洁的冲突分析子句。求解器可以根据这些包含更多信息的冲突分析子句在后续搜索中更加有效地避免冲突，以便更快的得到计算结果。
　　 2．研究相关的预处理算法，并对其有所改进。新设计预处理算法主要是为了在正式开始求解过程之前，对已有的CNF进行化简。由于现在流行的可满足性求解器的设计特点，其效率的高低对各个变量之间的逻辑关系的表达方式有着很强的依赖性，例如在CNF的子句中有大量的断言了句并且每个子句中所包含的文字尽量少会对快速解决问题有很大帮助。这也是本文所设计算法的出发点。
　　 3．研究设计了一种将SMT求解应用于最忧化问题的方法，使得原有的SMT求解器可以解决一定形式的最优化问题，并对其进行计算。该方法是使用数学中有关多元函数的极值必要条件的定理将一个最优化问题和其约束转化成一个等价的SMT问题再加以解决，为SMT求解技术的应用提供了一种新的可行方法。
　　 在基于求解器SATEEn的基础上，我们使用C语言和lex&yacc实现了相关的算法设计并进行了实验，通过对实验结果的分析证明了设计算法的正确性和可行性。