High-Throughput SAT Sampling

• DOI: 10.48550/arxiv.2502.08673
• Publication Date: 2025-02-11
• Authors: Arash Ardakani; Minwoo Kang; Kevin He; Qijing Huang; John Wawrzynek
• Keywords: FOS: Computer and information sciences; Computer Science - Machine Learning; Artificial Intelligence (cs.AI); Computer Science - Artificial Intelligence; Machine Learning (cs.LG)

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 functions. It then leverages gradient-based optimization to guide search diverse set valid solutions. Our operates circuit structure refactored instances, reinterpreting problem as supervised regression task. This differentiable enables independent bit-wise operations each tensor element, allowing parallel execution learning processes. As result, achieve with significant runtime improvements ranging from $33.6\times$ $523.6\times$ over state-of-the-art heuristic samplers. We demonstrate superior performance through an extensive evaluation $60$ instances public domain benchmark suite utilized in previous studies.