We propose an incomplete algorithm for Maximum Satisfiability (MaxSAT) specifically designed to run on neural network accelerators such as GPUs and TPUs. Given a MaxSAT problem instance in conjunctive normal form, our procedure constructs a Restricted Boltzmann Machine (RBM) with an equilibrium distribution wherein the probability of a Boolean assignment is exponential in the number of clauses it satisfies. Block Gibbs sampling is used to stochastically search the space of assignments with parallel Markov chains. Since matrix multiplication is the main computational primitive for block Gibbs sampling in an RBM, our approach leads to an elegantly simple algorithm (40 lines of JAX) well-suited for neural network accelerators. Theoretical results about RBMs guarantee that the required number of visible and hidden units of the RBM scale only linearly with the number of variables and constant-sized clauses in the MaxSAT instance, ensuring that the computational cost of a Gibbs step scales reasonably with the instance size. Search throughput can be increased by batching parallel chains within a single accelerator as well as by distributing them across multiple accelerators. As a further enhancement, a heuristic based on unit propagation running on CPU is periodically applied to the sampled assignments. Our approach, which we term RbmSAT, is a new design point in the algorithm-hardware co-design space for MaxSAT. We present timed results on a subset of problem instances from the annual MaxSAT Evaluation's Incomplete Unweighted Track for the years 2018 to 2021. When allotted the same running time and CPU compute budget (but no TPUs), RbmSAT outperforms other participating solvers on problems drawn from three out of the four years' competitions. Given the same running time on a TPU cluster for which RbmSAT is uniquely designed, it outperforms all solvers on problems drawn from all four years.

翻译：我们提出了一种不完整算法，专为在GPU和TPU等神经网络加速器上运行而设计，用于求解最大可满足性问题（MaxSAT）。给定一个合取范式形式的MaxSAT实例，我们的过程构建了一个受限玻尔兹曼机（RBM），其平衡分布中布尔赋值的概率与其满足的子句数量呈指数关系。通过块吉布斯采样，利用并行马尔可夫链对赋值空间进行随机搜索。由于矩阵乘法是RBM中块吉布斯采样的主要计算基元，我们的方法实现了一个简洁的算法（40行JAX代码），非常适合神经网络加速器。关于RBM的理论结果保证了RBM所需显见单元和隐单元的数量仅随MaxSAT实例中变量和恒定大小子句的数量线性增长，从而确保吉布斯步骤的计算成本随实例规模合理扩展。搜索吞吐量可以通过在单个加速器内批处理并行链以及跨多个加速器分布链来提升。作为进一步增强，每轮采样后，在CPU上运行基于单元传播的启发式规则对采样赋值进行更新。我们将此方法命名为RbmSAT，这是MaxSAT算法-硬件协同设计领域的一个新设计点。我们展示了在2018至2021年MaxSAT年度评测不完全无权重赛道中部分问题实例的计时结果。在分配相同运行时间和CPU计算预算（但无TPU）的条件下，RbmSAT在三年竞赛中（共四年）的问题上优于其他参赛求解器。而在RbmSAT专为设计的TPU集群上分配相同运行时间时，它在所有四年竞赛的问题上均优于所有求解器。