Presentation
Late Breaking Results: Differential and Massively Parallel Sampling of SAT Formulas
DescriptionDiverse solutions to the Boolean satisfiability (SAT) problem are essential for thorough testing and verification of software and hardware designs, ensuring reliability and applicability to real-world scenarios. We introduce a novel differentiable sampling method, called DiffSampler, which employs gradient descent (GD) to learn diverse solutions to the SAT problem. By formulating SAT as a supervised multi-output regression task and minimizing its loss function using GD, our approach enables performing the learning operations in parallel, leading to GPU-accelerated sampling and comparable runtime performance w.r.t. heuristic samplers. We demonstrate that DiffSampler can generate diverse uniform-like solutions similar to conventional samplers.
Event Type
Late Breaking Results Poster
TimeWednesday, June 266:00pm - 7:00pm PDT
LocationLevel 2 Lobby