arXiv:2502.08673v1 GPU加速布尔可满足性（SAT）采样的新方法 摘要: 在这项工作中，我们提出了一种新的技术，用于GPU加速的布尔可满足性（SAT）采样。与传统的直接在合取范式（CNF）上操作的采样算法不同，我们的方法通过将SAT问题的逻辑约束转化成简化后的多级、多输出布尔函数来分解其CNF表示形式。然后，该方法利用基于梯度的优化来引导对多种有效解的搜索。我们的方法直接作用于分解后的SAT实例的电路结构上，重新将SAT问题视为一个监督多输出回归任务。这种可微分的技术允许对每个张量元素进行独立的位操作，从而实现学习过程的并行执行。因此，我们实现了在最先进启发式采样器上显著的运行时加速，加速范围从$33.6\times$到$523.6\times$。我们通过在前人研究中使用的公共领域基准套件中的$60$个实例上进行广泛的评估，展示了我们采样方法的优越性能。