计算机应用研究

作者：罗茂,陈润尧,黄意雯,吴歆韵,熊才权,柯远志,

单位：1.湖北工业大学计算机学院,武汉430068；2.华中科技大学计算机科学与技术学院,武汉430074；

关键词：布尔可满足性,基于电路的SAT求解器,冲突驱动子句学习,电子设计自动化,等价性验证,

基金：国家自然科学基金资助项目(62402164)；；

布尔可满足性问题（SAT）求解器在电子设计自动化（EDA）领域应用广泛。当前主流SAT求解器均需要使用合取范式（CNF）格式的算例作为输入，然而将电路的与逆图（AIG）编码为CNF格式会导致原始电路的结构受到破坏，从而影响电路等价验证问题的求解效率。为解决此问题，提出并实现了一种直接解析电路结构文件的电路SAT求解器。该求解器基于冲突驱动子句学习（CDCL）框架，融合电路结构特性，集成了学习门删除策略、重启机制、基于电路节点活跃度的分支策略。在ISCAS’85/89基准电路上进行的电路等价验证的实验表明，各优化模块显著提升了性能，特别是分支策略在多个电路上实现了超100倍的加速，验证了直接在电路上进行等价验证的可行性。

来源：2026年第5期

《计算机应用研究》期刊编辑部

查看计算机应用研究杂志2026年第5期