高通量SAT采样
High-Throughput SAT Sampling
AI总结：
提出一种GPU加速布尔可满足性（SAT）采样新技术，将CNF分解为简化布尔函数，通过梯度优化引导搜索，实现并行学习，在60个基准实例上较启发式采样器提速33.6-523.6倍。
摘要：
在这项工作中，我们提出了一种用于GPU加速布尔可满足性（SAT）采样的新技术。与直接对合取范式（CNF）进行操作的传统采样算法不同，我们的方法通过将SAT问题的CNF表示分解为简化的多级、多输出布尔函数来转换其逻辑约束。然后，它利用基于梯度的优化来引导搜索多样化的有效解集。我们的方法直接对重构SAT实例的电路结构进行操作，将SAT问题重新解释为监督式多输出回归任务。这种可微分技术支持对每个张量元素进行独立的按位操作，允许学习过程的并行执行。因此，与最先进的启发式采样器相比，我们实现了GPU加速采样，运行时间提升幅度从33.6倍到523.6倍不等。我们通过对先前研究中使用的公共领域基准套件中的60个实例进行广泛评估，证明了我们采样方法的优越性能。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
