EDA顶级会议DAC 2025放榜，中科院软件所约束求解研究室有4篇论文录用，跟大家汇报一下，研究成果都是EDA求解器和工具，分别为：电路SAT，模型检测，等价性验证，ATPG。

此处重点介绍一下电路SAT求解器 XSAT：
SAT求解器是EDA领域的核心计算引擎。目前业界常用基于CNF的SAT求解器，直接在电路层次进行求解的电路SAT有希望达到更好的效果。然而，由于历史原因（特别是SAT比赛规范），之前电路SAT求解器进展很少（大部分工作很老，而一些工作存在明显错误），仍然以伯克利ABC工具自带的电路SAT求解器为主要代表。

在之前文献常测的通用电路数据集以及更加困难的乘法电路上，团队研发的XSAT都大幅度（几倍到几十倍）领先已有电路SAT求解器和MiniSAT，比肩前沿CNF-SAT求解器Kissat，在测试的乘法电路验证问题的求解上优于Kissat。

XSAT代码已经开源：http://t.cn/A61THjnA

更多约束求解器和EDA工具，欢迎访问中科院软件所约束求解研究室的工具列表
http://t.cn/A61THjn2