用可微分电路重构实现GPU加速的布尔满足采样，速度提升超百倍。
High-Throughput SAT Sampling
- 将CNF公式重构成多级电路，转为可微分回归任务
- 在60个基准测试上提速33.6至523.6倍
- 适合需要海量解采样的形式验证与AI应用
本文提出一种基于GPU加速的布尔满足（SAT）采样新方法。不同于传统直接处理合取范式（CNF）的算法，该方法将SAT问题的逻辑约束通过因子分解重构为简化后的多级、多输出布尔函数，并利用基于梯度的优化引导生成多样化有效解。方法直接作用于重构后SAT实例的电路结构，将原问题重新定义为监督式多输出回归任务。该可微分框架支持每个张量元素的独立位操作，实现学习过程的并行化。实验在公开基准套件的60个实例上验证，相较当前最优启发式采样器，运行时间提升达33.6×至523.6×。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。