HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation

要約

ブール方程式の充足可能性 (略して SAT 問題として知られています) を効率的に決定することは、さまざまな産業上の問題において重要です。
最近、深層学習手法の出現により、SAT の解決を強化する大きな可能性がもたらされました。
しかし、この分野の進歩に対する大きな障壁となっているのは、大規模で現実的なデータセットが不足していることです。
現在公開されているデータセットの大部分は、ランダムに生成されるか、または非常に限定されたものであり、無関係な問題ファミリーからのサンプルがいくつかしか含まれていません。
これらのデータセットは、深層学習手法の有意義なトレーニングには不十分です。
これを考慮して、研究者は、実際の状況で遭遇する SAT の問題をより正確に反映するデータを作成するための生成手法の探索を開始しました。
これらの方法はこれまで、困難な SAT 問題を生成できないか、時間拡張性の障害に悩まされてきました。
この論文では、コアと呼ばれる、問題の「難しさ」の主な原因を特定し、操作することで、この両方に対処します。
これまでの研究の中にはコアに対処したものもありますが、従来のヒューリスティック コア検出技術の費用がかかるため、時間コストが許容できないほど高くなります。
グラフニューラルネットワークを使用した高速コア検出手順を紹介します。
私たちの経験的な結果は、解決が難しい問題を効率的に生成し、元の問題例の重要な属性を保持できることを示しています。
生成された合成 SAT 問題をデータ拡張設定で使用して、ソルバーの実行時間の予測を改善できることを実験によって示します。

要約(オリジナル)

Efficiently determining the satisfiability of a boolean equation — known as the SAT problem for brevity — is crucial in various industrial problems. Recently, the advent of deep learning methods has introduced significant potential for enhancing SAT solving. However, a major barrier to the advancement of this field has been the scarcity of large, realistic datasets. The majority of current public datasets are either randomly generated or extremely limited, containing only a few examples from unrelated problem families. These datasets are inadequate for meaningful training of deep learning methods. In light of this, researchers have started exploring generative techniques to create data that more accurately reflect SAT problems encountered in practical situations. These methods have so far suffered from either the inability to produce challenging SAT problems or time-scalability obstacles. In this paper we address both by identifying and manipulating the key contributors to a problem’s “hardness”, known as cores. Although some previous work has addressed cores, the time costs are unacceptably high due to the expense of traditional heuristic core detection techniques. We introduce a fast core detection procedure that uses a graph neural network. Our empirical results demonstrate that we can efficiently generate problems that remain hard to solve and retain key attributes of the original example problems. We show via experiment that the generated synthetic SAT problems can be used in a data augmentation setting to provide improved prediction of solver runtimes.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google