# Circuit-Aware SAT Solving: Guiding CDCL via Conditional Probabilities

arXiv: https://arxiv.org/abs/2508.04235 · HTML: https://mlsanity.com/paper/2508.04235/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 27 references that are in the map.
- First posted on arXiv 6 Aug 2025.

## Builds on (most cited first, 7 of 7)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [DeepGate2: Functionality-Aware Circuit Representation Learning](https://mlsanity.com/paper/2305.16373/) (2023)
- [DeepGate3: Towards Scalable Circuit Representation Learning](https://mlsanity.com/paper/2407.11095/) (2024)
- [NetTAG: A Multimodal RTL-and-Layout-Aligned Netlist Foundation Model via Text-Attributed Graph](https://mlsanity.com/paper/2504.09260/) (2025)
- [Circuit Representation Learning with Masked Gate Modeling and Verilog-AIG Alignment](https://mlsanity.com/paper/2502.12732/) (2025)
- [Logic Optimization Meets SAT: A Novel Framework for Circuit-SAT Solving](https://mlsanity.com/paper/2403.19446/) (2024)

## Built on by (most cited first, 2 of 2)

- [CLUE: Conflict-guided Localization for LLM Unlearning Framework](https://mlsanity.com/paper/2509.20977/) (2025)
- [Beyond Flat Netlist: Hierarchical Graph Representation Learning for Scalable Analysis of Sequential Circuits](https://mlsanity.com/paper/2608.28188/) (2026)

## Abstract (arXiv)

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.