NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks

要約

命題充足可能性 (SAT) は、計画、検証、セキュリティなどの多くの研究分野に影響を与える NP 完全問題です。
主流の最新の SAT ソルバーは、Conflict-Driven Clause Learning (CDCL) アルゴリズムに基づいています。
最近の研究は、グラフ ニューラル ネットワーク (GNN) を使用して CDCL SAT ソルバーを強化することを目的としています。
ただし、これまでのところ、このアプローチでは解決の効率が向上していないか、頻繁なオンライン モデル推論に大量の GPU リソースが必要です。
GNN の改善を実用化することを目指して、この論文は NeuroBack と呼ばれるアプローチを提案します。これは 2 つの洞察に基づいています: (1) 満足のいく割り当ての大部分 (またはすべて) に現れる変数のフェーズ (つまり、値) を予測することは、CDCL にとって不可欠です。
(2) SAT 解決を開始する前に、予測のためにニューラル モデルに 1 回だけクエリを実行するだけで十分です。
トレーニングが完了すると、オフライン モデル推論により、NeuroBack が CPU 上で排他的に実行できるようになり、GPU リソースへの依存がなくなります。
NeuroBack をトレーニングするには、120,286 個のデータ サンプルを含む DataBack と呼ばれる新しいデータセットが作成されます。
最後に、NeuroBack は、Kissat と呼ばれる最先端の SAT ソルバーの拡張機能として実装されています。
その結果、Kissat は、最近の SAT コンペティション問題集である SATCOMP-2022 の問題を 5.2% 多く解くことができました。
したがって、NeuroBack は、機械学習を利用して SAT の解決を効果的かつ実践的に改善する方法を示します。

要約(オリジナル)

Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Mainstream modern SAT solvers are based on the Conflict-Driven Clause Learning (CDCL) algorithm. Recent work aimed to enhance CDCL SAT solvers using Graph Neural Networks (GNNs). However, so far this approach either has not made solving more effective, or required substantial GPU resources for frequent online model inferences. Aiming to make GNN improvements practical, this paper proposes an approach called NeuroBack, which builds on two insights: (1) predicting phases (i.e., values) of variables appearing in the majority (or even all) of the satisfying assignments are essential for CDCL SAT solving, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts. Once trained, the offline model inference allows NeuroBack to execute exclusively on the CPU, removing its reliance on GPU resources. To train NeuroBack, a new dataset called DataBack containing 120,286 data samples is created. Finally, NeuroBack is implemented as an enhancement to a state-of-the-art SAT solver called Kissat. As a result, it allowed Kissat to solve 5.2% more problems on the recent SAT competition problem set, SATCOMP-2022. NeuroBack therefore shows how machine learning can be harnessed to improve SAT solving in an effective and practical manner.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google