Addressing Variable Dependency in GNN-based SAT Solving

要約

タイトル – GNNを利用したSATソルバーにおける可変依存性の解決
要約 –
– SAT問題は多くのアプリケーションにおいて基礎的な問題である。
– GNN（グラフニューラルネットワーク）を（近似）SATソルバーに利用することが先行研究において行われている。
– 一般的なGNNに基づくSATソルバーはSAT解を同時に予測するが、クラスタリングされた複数のSAT問題に対して、同時予測が正しい答えを生成できないことを示す。
– 著者たちは、AsymSATというGNNベースのアーキテクチャを提案し、再帰ニューラルネットワークを統合して、可変の割り当てに依存した予測を生成することで、可変変数の依存関係を考慮している。
– 実験結果は、依存関係のある可変の予測によって、GNNに基づく方法の解決能力が拡張され、大規模テストセット上で解決されたSATインスタンスの数が向上することを示している。

要約(オリジナル)

Boolean satisfiability problem (SAT) is fundamental to many applications. Existing works have used graph neural networks (GNNs) for (approximate) SAT solving. Typical GNN-based end-to-end SAT solvers predict SAT solutions concurrently. We show that for a group of symmetric SAT problems, the concurrent prediction is guaranteed to produce a wrong answer because it neglects the dependency among Boolean variables in SAT problems. % We propose AsymSAT, a GNN-based architecture which integrates recurrent neural networks to generate dependent predictions for variable assignments. The experiment results show that dependent variable prediction extends the solving capability of the GNN-based method as it improves the number of solved SAT instances on large test sets.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI