Circuit-Aware SAT Solving: Guiding CDCL via Conditional Probabilities

• URL: http://arxiv.org/abs/2508.04235v1
• Date: Wed, 06 Aug 2025 09:16:47 GMT
• Title: Circuit-Aware SAT Solving: Guiding CDCL via Conditional Probabilities
• Authors: Jiaying Zhu, Ziyang Zheng, Zhengyuan Shi, Yalun Cai, Qiang Xu,
• Abstract summary: Circuit Satisfiability (CSAT) plays a pivotal role in Electronic Design Automation.<n>We introduce CASCAD, a novel circuit-aware SAT solving framework.<n>We show that CASCAD reduces solving times by up to 10x compared to state-of-the-art CNF-based approaches.
• Score: 8.18310731992061
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs [2.722939308105689]
  This work introduces Reinforcement Learning from Algorithm Feedback (RLAF) as a paradigm for learning to guide SAT solver branchings with Graph Neural Networks (GNNs)<n> RLAF-trained policies significantly reduce the mean solve times of different base solvers across diverse SAT problem distributions, achieving more than a 2x speedup in some cases.
  arXiv  Detail & Related papers  (2025-05-21T22:07:08Z)
• Architect of the Bits World: Masked Autoregressive Modeling for Circuit Generation Guided by Truth Table [5.300504429005315]
  We propose a novel approach integrating conditional generative models with differentiable architecture search (DAS) for circuit generation.<n>Our approach first introduces CircuitVQ, a circuit tokenizer trained based on our Circuit AutoEncoder.<n>We then develop CircuitAR, a masked autoregressive model leveraging CircuitVQ as the tokenizer.
  arXiv  Detail & Related papers  (2025-02-18T11:13:03Z)
• Bayesian Parameterized Quantum Circuit Optimization (BPQCO): A task and hardware-dependent approach [49.89480853499917]
  Variational quantum algorithms (VQA) have emerged as a promising quantum alternative for solving optimization and machine learning problems. In this paper, we experimentally demonstrate the influence of the circuit design on the performance obtained for two classification problems. We also study the degradation of the obtained circuits in the presence of noise when simulating real quantum computers.
  arXiv  Detail & Related papers  (2024-04-17T11:00:12Z)
• An Efficient Learning-based Solver Comparable to Metaheuristics for the Capacitated Arc Routing Problem [67.92544792239086]
  We introduce an NN-based solver to significantly narrow the gap with advanced metaheuristics. First, we propose direction-aware facilitating attention model (DaAM) to incorporate directionality into the embedding process. Second, we design a supervised reinforcement learning scheme that involves supervised pre-training to establish a robust initial policy.
  arXiv  Detail & Related papers  (2024-03-11T02:17:42Z)
• AutoSAT: Automatically Optimize SAT Solvers via Large Language Models [10.359005620433136]
  We propose AutoSAT, a framework that automatically optimizes in a pre-defined modular search space based on existing CDCL solvers. A realization of AutoSAT outperforms MiniSat on 9 out of 12 datasets and even surpasses the state-of-the-art hybrid solver Kissat on 4 datasets.
  arXiv  Detail & Related papers  (2024-02-16T14:04:56Z)
• Transformers as Statisticians: Provable In-Context Learning with In-Context Algorithm Selection [88.23337313766353]
  This work first provides a comprehensive statistical theory for transformers to perform ICL. We show that transformers can implement a broad class of standard machine learning algorithms in context. A emphsingle transformer can adaptively select different base ICL algorithms.
  arXiv  Detail & Related papers  (2023-06-07T17:59:31Z)
• Actor-Critic based Improper Reinforcement Learning [61.430513757337486]
  We consider an improper reinforcement learning setting where a learner is given $M$ base controllers for an unknown Markov decision process. We propose two algorithms: (1) a Policy Gradient-based approach; and (2) an algorithm that can switch between a simple Actor-Critic scheme and a Natural Actor-Critic scheme.
  arXiv  Detail & Related papers  (2022-07-19T05:55:02Z)
• Efficient Quantum Circuit Design with a Standard Cell Approach, with an Application to Neutral Atom Quantum Computers [45.66259474547513]
  We design quantum circuits by using the standard cell approach borrowed from classical circuit design. We present evidence that, when compared with automatic routing methods, our layout-aware routers are significantly faster and achieve shallower 3D circuits.
  arXiv  Detail & Related papers  (2022-06-10T10:54:46Z)
• Efficient Knowledge Compilation Beyond Weighted Model Counting [7.828647825246474]
  We introduce Second Level Algebraic Model Counting (2AMC) as a generic framework for these kinds of problems. First level techniques based on Knowledge Compilation (KC) have been adapted for specific 2AMC instances by imposing variable order constraints. We show that we can exploit the logical structure of a 2AMC problem to omit parts of these constraints, thus limiting the negative effect.
  arXiv  Detail & Related papers  (2022-05-16T08:10:40Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• On Continuous Local BDD-Based Search for Hybrid SAT Solving [40.252804008544985]
  We propose a novel algorithm for efficiently computing the gradient needed by CLS. We study the capabilities and limitations of our versatile CLS solver, GradSAT, by applying it on many benchmark instances. The experimental results indicate that GradSAT can be a useful addition to the portfolio of existing SAT and MaxSAT solvers for solving Boolean satisfiability and optimization problems.
  arXiv  Detail & Related papers  (2020-12-14T22:36:20Z)
• Combining Deep Learning and Optimization for Security-Constrained Optimal Power Flow [94.24763814458686]
  Security-constrained optimal power flow (SCOPF) is fundamental in power systems. Modeling of APR within the SCOPF problem results in complex large-scale mixed-integer programs. This paper proposes a novel approach that combines deep learning and robust optimization techniques.
  arXiv  Detail & Related papers  (2020-07-14T12:38:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.