TLDR: CASCAD is a new framework that improves Circuit Satisfiability (CSAT) solving by using Graph Neural Networks (GNNs) to calculate real-time conditional probabilities from circuit structures. This dynamic guidance helps standard SAT solvers make better decisions for variable assignments and manage learned clauses, leading to significantly faster solving times (up to 10x) on complex electronic design automation (EDA) problems compared to traditional methods.
In the world of Electronic Design Automation (EDA), a critical challenge is Circuit Satisfiability (CSAT). This involves determining if a given electronic circuit can produce a ‘true’ output for some set of inputs. Traditionally, CSAT problems are converted into a format called Conjunctive Normal Form (CNF) and then solved using powerful SAT solvers, particularly those based on Conflict-Driven Clause Learning (CDCL).
However, this conversion process has a significant drawback: it discards valuable structural and functional information inherent in the original circuit. This loss of information often leads to less-than-optimal performance from the SAT solvers.
Addressing this limitation, researchers have introduced a novel framework called CASCAD (Circuit-Aware SAT Solving via Conditional Probability-Guided Decisions). CASCAD aims to bridge the gap between static circuit structures and the dynamic decision-making process of CDCL solvers. It does this by directly leveraging circuit-level conditional probabilities, which are computed using advanced Graph Neural Networks (GNNs).
How CASCAD Works
CASCAD dynamically guides two crucial CDCL heuristics: variable phase selection and clause management. Variable phase selection involves deciding whether to assign a variable as ‘true’ or ‘false’ during the solving process. CASCAD uses conditional probabilities to favor assignments that are more likely to lead to a satisfying solution, thereby accelerating the search and reducing conflicts.
For clause management, CASCAD proposes a new metric: clause probability. Learned clauses, which are derived from conflicts, are essential for pruning the search space. Traditional methods rely on metrics that ignore the circuit’s structural insights. CASCAD, however, estimates the likelihood of a clause being satisfied based on circuit-level signal estimations. Clauses with lower probabilities are considered stronger constraints and are prioritized, helping the solver focus on more informative parts of the problem.
The framework employs a two-stage training strategy for its GNN model. The first stage uses pattern-based pre-training to capture fine-grained circuit behavior, while the second stage uses workload-aware fine-tuning to generalize to broader statistical distributions. This robust training ensures high accuracy in predicting gate-level conditional probabilities, achieving a validation accuracy of 96.69%.
Also Read:
- Deliberative Reasoning Networks: A New Path to Logical AI
- Evaluating Trust in AI: A New Benchmark for Multimodal Model Confidence
Significant Performance Gains
Extensive evaluations on challenging, real-world Logical Equivalence Checking (LEC) benchmarks have demonstrated CASCAD’s effectiveness. The framework has shown remarkable improvements in solving times, reducing them by up to 10 times compared to state-of-the-art CNF-based approaches. Furthermore, the probability-guided clause filtering strategy alone contributed an additional 23.5% runtime reduction.
The research highlights the importance of preserving circuit-level structural insights within SAT solvers. Even when strong preprocessing techniques are applied, CASCAD’s dynamic guidance during the in-processing stage provides substantial additional speedups, proving its complementary and essential role.
This work not only advances the theoretical understanding of how structural information can be leveraged in SAT solving but also provides a robust foundation for future enhancements in SAT-solving efficiency and EDA tool design. For more in-depth details, you can read the full research paper here.
