球友会qy发布新型电路SAT求解器----中国科研实验室软件研究所

球友会qy发布新型电路SAT求解器

文章来源： | 发布时间：2025-03-04 | 【打印】【关闭】

近期，中国科研实验室软件研究所基础软件与系统重点实验室约束求解研究室论文X-SAT: An Efficient Circuit-Based-SAT-Solver被EDA领域顶级会议DAC 2025接收，第一作者为硕士生钱宇航，通讯作者为蔡少伟研究员。论文提出了一种自主研发的电路SAT求解器——X-SAT，不含外部来源代码，其性能在常用数据集上大幅度领先现有电路SAT求解器，提升了约束求解技术在电路场景中的实用性，有望在更多电子设计自动化（EDA）问题以及密码分析等领域中发挥价值。该工作取得了中国科研实验室先导A专项“RISC－V基础软件”支持。

布尔可满足性问题（SAT）是计算机科学的核心问题之一。SAT求解器作为EDA领域的核心计算引擎，通常采取合取范式（CNF）格式，在处理电路相关问题时，需要先将电路编码为CNF公式再进行求解。相比之下，电路SAT求解直接以门级网表为输入、以门结构为基本推理单元，能够更贴近电路结构，利用电路中更多的门级信息来进行搜索、推理和学习。然而，由于SAT比赛赛制等历史原因，电路SAT求解技术的研究工作较少且进展缓慢。当前具有代表性的电路SAT求解器CBS，由加州大学伯克利分校逻辑验证综合工具ABC集成，实测求解性能相较前沿CNF求解器kissat仍有较大差距。

约束求解研究室科研团队提出的电路SAT求解器X-SAT，主要包含电路重写模块和电路CDCL求解模块两部分。其中，科研团队在重写模块创新性地提出了一种只包含XOR门和LUT门的门级网表XLG，相比传统AIG结构可大幅减少逻辑门数量；在电路CDCL求解模块，科研团队在XLG门上执行传播推理及子句学习等技术，并基于XLG的紧凑电路表示改进了变量的打分策略，提出了变元搜索启发式XVSIDS。

X-SAT框架图

测试结果显示，在学术通用电路数据集ISCAS85、ISCAS89和ITC99上，X－SAT对比国际先进的电路SAT求解器，实现了7.08倍的加速。在更困难的乘加混合电路上，X－SAT大幅领先已有电路SAT求解器和轻量求解器MiniSat，分别实现了36.34倍和50.99倍的加速。并首次超过了主流基于CNF的SAT求解器kissat，提高性能达35.94％。

约束求解研究室此次共有4篇论文被DAC　2025会议录用，除了提出电路SAT求解器，另外3篇论文分别涉及模型检查工具（一作为硕士生朱凌峰，通讯作者为李勇坚副研究员）、并行图划分等价性验证工具（蔡少伟为共同通讯作者）和基于部分解SAT求解器的ATPG工具（特别研究助理张昕荻为共同一作，蔡少伟为共同通讯作者）。

球友会qy约束求解研究室专注于约束求解与形式化方法的算法研究和实际应用，研发的约束求解器多次取得SAT、SMT、MaxSAT等约束求解领域重要比赛冠军，CAV、SAT、CP等顶级会议荣获最佳／杰出论文奖，并且开源了多款求解器和EDA工具的代码，成果应用于EDA、操作系统、云计算、互联网、信息安全等领域并发挥了重要经济价值。