Denoising Diffusion for Sampling SAT Solutions
This addresses the need for diverse SAT solutions in testing and verification, but is incremental as it builds on existing neural methods.
The paper tackled the problem of generating diverse solutions to the Boolean Satisfiability Problem (SAT) for applications in software and hardware testing, using Denoising Diffusion with a Graph Neural Network, achieving accuracy similar to the best neural method and producing highly diverse solutions.
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.