The Boolean Satisfiability problem (SAT) is the most prototypical NP-complete
problem and of great practical relevance. One important class of solvers for
this problem are stochastic local search (SLS) algorithms that iteratively and
randomly update a candidate assignment. Recent breakthrough results in
theoretical computer science have established sufficient conditions under which
SLS solvers are guaranteed to efficiently solve a SAT instance, provided they
have access to suitable "oracles" that provide samples from an
instance-specific distribution, exploiting an instance's local structure.
Motivated by these results and the well established ability of neural networks
to learn common structure in large datasets, in this work, we train oracles
using Graph Neural Networks and evaluate them on two SLS solvers on random SAT
instances of varying difficulty. We find that access to GNN-based oracles
significantly boosts the performance of both solvers, allowing them, on
average, to solve 17% more difficult instances (as measured by the ratio
between clauses and variables), and to do so in 35% fewer steps, with
improvements in the median number of steps of up to a factor of 8. As such,
this work bridges formal results from theoretical computer science and
practically motivated research on deep learning for constraint satisfaction
problems and establishes the promise of purpose-trained SAT solvers with
performance guarantees.

利用图神经网络训练适用于布尔可满足性问题的 SLS 求解器，可显著提高性能，平均解决比例更高、步骤更少，具有性能保证。

利用深度学习构建带性能界限的随机局部搜索 SAT 求解器

Using deep learning to construct stochastic local search SAT solvers  with performance bounds

Recent work proposed the UCTMAXSAT algorithm to address Maximum
Satisfiability Problems (MaxSAT) and shown improved performance over pure
Stochastic Local Search algorithms (SLS). UCTMAXSAT is based on Monte Carlo
Tree Search but it uses SLS instead of purely random playouts. In this work, we
introduce two algorithmic variations over UCTMAXSAT. We carry an empirical
analysis on MaxSAT benchmarks from recent competitions and establish that both
ideas lead to performance improvements. First, a nesting of the tree search
inspired by the Nested Monte Carlo Search algorithm is effective on most
instance types in the benchmark. Second, we observe that using a static flip
limit in SLS, the ideal budget depends heavily on the instance size and we
propose to set it dynamically. We show that it is a robust way to achieve
comparable performance on a variety of instances without requiring additional
tuning.

本文介绍了针对最大可满足性问题提出的 UCTMAXSAT 算法，探讨了两种算法变化对算法性能的影响，提出了使用静态翻转限制并动态设置预算来达到相似性能的建议。