Denoising Diffusion for Sampling SAT Solutions

Understand

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.