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

Visual layouts of graphs representing SAT instances can highlight the
community structure of SAT instances. The community structure of SAT instances
has been associated with both instance hardness and known clause quality
heuristics. Our tool SATViz visualizes CNF formulas using the variable
interaction graph and a force-directed layout algorithm. With SATViz, clause
proofs can be animated to continuously highlight variables that occur in a
moving window of recently learned clauses. If needed, SATViz can also create
new layouts of the variable interaction graph with the adjusted edge weights.
In this paper, we describe the structure and feature set of SATViz. We also
present some interesting visualizations created with SATViz.

SATViz 是利用变量交互图和力导向布局算法可视化 CNF 公式，能动态高亮显示最近学习子句中出现的变量，实现生成可调整边权重的变量交互图布局，在本文中介绍了 SATViz 的结构和特性，并展示了一些有趣的可视化效果。

SATViz: Clausal Proofs 实时可视化

SATViz: Real-Time Visualization of Clausal Proofs

In recent years, portfolio approaches to solving SAT problems and CSPs have
become increasingly common. There are also a number of different encodings for
representing CSPs as SAT instances. In this paper, we leverage advances in both
SAT and CSP solving to present a novel hierarchical portfolio-based approach to
CSP solving, which we call Proteus, that does not rely purely on CSP solvers.
Instead, it may decide that it is best to encode a CSP problem instance into
SAT, selecting an appropriate encoding and a corresponding SAT solver. Our
experimental evaluation used an instance of Proteus that involved four CSP
solvers, three SAT encodings, and six SAT solvers, evaluated on the most
challenging problem instances from the CSP solver competitions, involving
global and intensional constraints. We show that significant performance
improvements can be achieved by Proteus obtained by exploiting alternative
view-points and solvers for combinatorial problem-solving.

该论文提出了一种名为 Proteus 的分层组合策略解决 CSP 问题的方法，该方法能够将 CSP 实例编码为 SAT 形式，并选择合适的编码和相应的 SAT 求解器进行求解，实验结果表明 Proteus 能够显著提高组合问题求解性能。