Circuit-Aware SAT Solving: Guiding CDCL via Conditional Probabilities

TL;DR

CASCAD introduces a circuit-aware SAT solver that utilizes circuit-level conditional probabilities via GNNs to guide CDCL heuristics, significantly improving solving efficiency on real-world benchmarks.

Contribution

This work presents a novel framework that directly incorporates circuit structural information into SAT solving, enhancing performance over traditional CNF-based methods.

Findings

Up to 10x faster solving times on real-world benchmarks.

23.5% additional runtime reduction through probability-guided clause filtering.

Effective use of GNNs to model gate-level conditional probabilities.

Abstract

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.