Denoising Diffusion for Sampling SAT Solutions

2022/11/30 by Kārlis Freivalds, Freivalds, Karlis, Sergejs Kozlovičs +1 · 1 citation
Computer Science · Engineering · Materials Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Integrated Circuits and Semiconductor Failure Analysis #Machine Learning (cs.LG) #Machine Learning in Materials Science #VLSI and Analog Circuit Testing

paper · pdf · doi:10.48550/arxiv.2212.00121

openalex publication_date 2022/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

Generating diverse solutions to the Boolean Satisfiability Problem (SAT) is a hard computational problem with practical applications for testing and functional verification of software and hardware designs. We explore the way to generate such solutions using Denoising Diffusion coupled with a Graph Neural Network to implement the denoising function. We find that the obtained accuracy is similar to the currently best purely neural method and the produced SAT solutions are highly diverse, even if the system is trained with non-random solutions from a standard solver.

Cited by

• A Geometric Perspective on the Difficulties of Learning GNN-based SAT Solvers

Related

• DIFUSCO: Graph-based Diffusion Solvers for Combinatorial Optimization
• Deep Networks as Denoising Algorithms: Sample-Efficient Learning of Diffusion Models in High-Dimensional Graphical Models
• The Missing U for Efficient Diffusion Models
• GENIE: Higher-Order Denoising Diffusion Solvers
• Simple and Critical Iterative Denoising: A Recasting of Discrete Diffusion in Graph Generation