用图神经网络指导电路求解，速度提升10倍。
Circuit-Aware SAT Solving: Guiding CDCL via Conditional Probabilities
- 通过GNN计算门级条件概率，动态优化求解策略。
- 在真实电路等价性检查中，求解时间减少最多10倍。
- 适合需要高效电路验证的EDA工具开发者。
电路可满足性（CSAT）在电子设计自动化中至关重要。传统方法将电路转换为合取范式（CNF），并使用基于冲突驱动子句学习（CDCL）的通用求解器，但此过程会丢失丰富的结构与功能信息，导致性能不佳。为此，我们提出CASCAD——一种新型电路感知的求解框架，直接利用图神经网络（GNN）计算的电路级条件概率，显式建模门级条件概率，动态引导两个关键的CDCL启发式策略：变量相位选择和子句管理，显著提升求解效率。在具有挑战性的实际电路等价性检查（LEC）基准测试中，与最先进的基于CNF的方法相比，CASCAD将求解时间减少了高达10倍，并通过概率引导的子句过滤策略额外降低了23.5%的运行时间。结果表明，在SAT求解器中保留电路级结构信息至关重要，为未来提高求解效率和EDA工具设计提供了坚实基础。
原文摘要 · Abstract (English)
Circuit Satisfiability (CSAT) plays a pivotal role in Electronic Design Automation. The standard workflow for solving CSAT problems converts circuits into Conjunctive Normal Form (CNF) and employs generic SAT solvers powered by Conflict-Driven Clause Learning (CDCL). However, this process inherently discards rich structural and functional information, leading to suboptimal solver performance. To address this limitation, we introduce CASCAD, a novel circuit-aware SAT solving framework that directly leverages circuit-level conditional probabilities computed via Graph Neural Networks (GNNs). By explicitly modeling gate-level conditional probabilities, CASCAD dynamically guides two critical CDCL heuristics -- variable phase selection and clause managementto significantly enhance solver efficiency. Extensive evaluations on challenging real-world Logical Equivalence Checking (LEC) benchmarks demonstrate that CASCAD reduces solving times by up to 10x compared to state-of-the-art CNF-based approaches, achieving an additional 23.5% runtime reduction via our probability-guided clause filtering strategy. Our results underscore the importance of preserving circuit-level structural insights within SAT solvers, providing a robust foundation for future improvements in SAT-solving efficiency and EDA tool design.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。