Speaker
Description
The Boolean Satisfiability Problem (SAT) is a foundational problem in computer science with applications across a wide range of domains. Because SAT solvers exhibit varying behavior across different problem classes, the ability to generate synthetic SAT instances is valuable for benchmarking and solver-specific analysis. Recent methods have introduced Deep Learning approaches into this process, but these approaches often produce trivial instances or limit the sample space by only copying and perturbing existing formulas.
In this work, we propose a novel approach to SAT instance generation using latent graph diffusion models. We adapt this framework to the bipartite graph structure of SAT formulas and introduce an architecture that leverages meta-path connections to improve message passing between nodes of the same type. This design allows us to generate instances that strike a balance between structural similarity, solver-level complexity, and instance-level uniqueness of a given class. Early experiments on smaller benchmark domains (e.g. graph coloring encodings) indicate that this trade-off between hardness and novelty can be effectively achieved.
Finally, our diffusion-based formulation is designed to support conditional generation, with the goal of enabling explicit control over the satisfiability of generated instances. To our knowledge, Diff2SAT would be the first neural SAT generator with this capability. Further evaluation on larger, real-world formulas is ongoing.
