Circuit-Aware SAT Solving: Guiding CDCL via Conditional Probabilities
This work addresses performance bottlenecks in Electronic Design Automation for engineers, offering a significant but incremental improvement over existing CNF-based methods.
The paper tackled the problem of inefficient SAT solving for circuit satisfiability by introducing CASCAD, a circuit-aware framework that uses GNN-computed conditional probabilities to guide CDCL heuristics, resulting in up to 10x faster solving times and a 23.5% runtime reduction from clause filtering.
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.