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）算法，该算法通过构建具有指数数量布尔赋值的平衡分布的受限玻尔兹曼机（RBM）来解决 MaxSAT 问题，使用并行马尔可夫链中的块 Gibbs 采样来随机搜索赋值空间，同时通过在 CPU 上运行基于单位传播的启发式算法对采样的赋值进行定期优化。我们的方法在 MaxSAT 的算法硬件协同设计空间中提供了一个新的设计点，并且在各年度 MaxSAT 评估竞赛的部分问题实例中显示出出色的表现。