Denoising Diffusion for Sampling SAT Solutions

TL;DR

This paper introduces a novel approach combining denoising diffusion and graph neural networks to generate diverse SAT solutions, matching state-of-the-art accuracy while enhancing solution diversity.

Contribution

It presents a new method that leverages denoising diffusion models with GNNs for SAT solution generation, improving diversity without sacrificing accuracy.

Findings

Achieves accuracy comparable to the best neural methods

Produces highly diverse SAT solutions

Works with non-random solutions from standard solvers

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.