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

要約

ブール充足可能性問題 (SAT) は、最も典型的な NP 完全問題であり、実用的な関連性が非常に高いです。
この問題に対するソルバーの重要なクラスの 1 つは、候補割り当てを反復的かつランダムに更新する確率的局所探索 (SLS) アルゴリズムです。
理論的コンピューターサイエンスにおける最近の画期的な成果により、SLS ソルバーがインスタンス固有のディストリビューションからサンプルを提供し、インスタンスのローカル構造を利用してサンプルを提供する適切な「オラクル」にアクセスできるという条件で、SLS ソルバーが SAT インスタンスを効率的に解決することが保証される十分な条件が確立されました。
これらの結果と、大規模なデータセット内の共通構造を学習するニューラル ネットワークの確立された能力に動機付けられ、この研究では、グラフ ニューラル ネットワークを使用してオラクルをトレーニングし、さまざまな難易度のランダムな SAT インスタンスに対して 2 つの SLS ソルバーでオラクルを評価します。
GNN ベースのオラクルにアクセスすると、両方のソルバーのパフォーマンスが大幅に向上し、平均して 17% より困難なインスタンス (節と変数の比率で測定) を解決できるようになり、35% 少ない処理で解決できることがわかりました。
ステップ数の中央値は最大 8 倍に改善されています。このように、この研究は、理論的なコンピューターサイエンスと、制約充足問題のための深層学習に関する実践的な動機に基づいた研究からの正式な結果を橋渡しし、目的に合わせてトレーニングされた SAT の約束を確立します。
パフォーマンスが保証されたソルバー。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google