High-Throughput SAT Sampling
This work addresses the need for faster SAT sampling in computational logic and verification, offering a significant speedup but is incremental as it builds on existing sampling methods with a novel optimization approach.
The paper tackles the problem of Boolean satisfiability (SAT) sampling by introducing a GPU-accelerated technique that transforms CNF constraints into simplified Boolean functions and uses gradient-based optimization, achieving runtime improvements of 33.6× to 523.6× over state-of-the-art heuristic samplers.
In this work, we present a novel technique for GPU-accelerated Boolean satisfiability (SAT) sampling. Unlike conventional sampling algorithms that directly operate on conjunctive normal form (CNF), our method transforms the logical constraints of SAT problems by factoring their CNF representations into simplified multi-level, multi-output Boolean functions. It then leverages gradient-based optimization to guide the search for a diverse set of valid solutions. Our method operates directly on the circuit structure of refactored SAT instances, reinterpreting the SAT problem as a supervised multi-output regression task. This differentiable technique enables independent bit-wise operations on each tensor element, allowing parallel execution of learning processes. As a result, we achieve GPU-accelerated sampling with significant runtime improvements ranging from $33.6\times$ to $523.6\times$ over state-of-the-art heuristic samplers. We demonstrate the superior performance of our sampling method through an extensive evaluation on $60$ instances from a public domain benchmark suite utilized in previous studies.