随着集成电路技术和制造技术不断进步，电路的规模也不断增大，电路验证领域面临着前所未有的挑战。传统的基于模拟的验证方法不能满足电路复杂度增大的需要，具有完备性特点的形式化验证方法开始得到人们的关注，成为当前的研究热点。 本文研究工作是针对组合电路的等价验证展开的。由于近些年来，作为验证基本问题的可满足性问题(SAT)研究取得了重大进展，有效的SAT解算器诸如zChaff，BerkMin和C．SAT等已可解决很大规模SAT问题，并且作为一个优秀搜索引擎在电路验证问题方面有着广泛应用。本文分析了现有的电路可满足性验证工具的优缺点，针对验证中学习效率的瓶颈提出了改进的方法，能够更加合理地利用电路现有的信息。 本文主要的创新之处在于：(1)对待验证电路进行与／非图同构简化，合并待验证两电路的相似部分，以减小待验证电路产生的数据结构规模。(2)根据电路的拓扑结构，合理选择学习子句，避免重复无用的学习过程。(3)通过模拟蕴含学习，能够避免过深层次搜索，从而快速得到电路信息子句，以减少SAT推理的搜索空间。从实验分析表明，这些措施在有效地减少学习时间的同时，又保证了整体验证过程的完备性和高效率。