論文の概要: HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation
- arxiv url: http://arxiv.org/abs/2409.18778v1
- Date: Fri, 27 Sep 2024 14:24:16 GMT
- ステータス: 処理完了
- システム内更新日: 2024-10-01 11:53:50.456971
- Title: HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation
- Title（参考訳）: HardCore生成: データ拡張のためのハードUNSAT問題の生成
- Authors: Joseph Cotnareanu, Zhanguang Zhang, Hui-Ling Zhen, Yingxue Zhang, Mark Coates,
- Abstract要約: SAT問題(SAT problem for brevity)として知られる方程式の満足度を効果的に決定することは、様々な産業問題において重要である。
深層学習手法はSAT問題解決に重要な可能性をもたらした。
この分野での進歩の大きな障壁は、大規模で現実的なデータセットの不足である。
- 参考スコア（独自算出の注目度）: 18.610223458286953
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
- Abstract（参考訳）: SAT問題(SAT problem for brevity)として知られるブール方程式の満足度を効果的に決定することは、様々な産業問題において重要である。
近年、深層学習法が出現し、SAT問題解決に大きな可能性をもたらしている。
しかし、この分野の発展の大きな障壁は、大規模で現実的なデータセットの不足である。
現在の公開データセットの大部分はランダムに生成されているか、非常に制限されている。
これらのデータセットは、ディープラーニングメソッドの有意義なトレーニングには不十分である。
これを踏まえて、研究者はSAT問題をより正確に反映したデータを生成するための生成技術を模索し始めた。
これらの手法は、これまでSAT問題や時間スケール性障害を発生させることができないかに悩まされてきた。
本稿では、コアとして知られる問題の「硬さ」に寄与する重要なコントリビュータを特定し、操作することで対処する。
これまでのいくつかの研究はコアに対処してきたが、従来のヒューリスティックコア検出技術に費やされているため、時間コストは許容できないほど高い。
本稿では,グラフニューラルネットワークを用いた高速コア検出手法を提案する。
実験結果から,解きづらい問題を効率よく生成し,元の例問題の鍵となる属性を維持できることが示唆された。
実験により,生成したSAT問題をデータ拡張設定に使用することにより,ソルバランタイムの予測精度の向上が期待できることを示す。
関連論文リスト
- Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。
これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。
私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
論文 参考訳（メタデータ） (2024-10-18T22:25:54Z) - Using deep learning to construct stochastic local search SAT solvers
with performance bounds [0.0]
グラフニューラルネットワークを用いてオーラクルを訓練し、2つのSLSソルバ上で、様々な難易度を持つランダムSATインスタンス上でそれらを評価する。
GNNベースのオラクルへのアクセスは,両者のパフォーマンスを著しく向上させることがわかった。
論文 参考訳（メタデータ） (2023-09-20T16:27:52Z) - W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs [11.139131079925113]
W2SATは、現実世界/産業インスタンスから固有の構造と特性を学ぶことによってSAT式を生成するフレームワークである。
Weighted Literal Incidence Graph (WLIG)と呼ばれる新しいSAT表現を導入する。
WLIGからSAT問題への復号化は、新しい丘登り最適化法で重なり合う斜角を見つけることをモデル化する。
論文 参考訳（メタデータ） (2023-02-01T06:30:41Z) - Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。
ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
論文 参考訳（メタデータ） (2022-03-02T05:14:12Z) - Generalization of Neural Combinatorial Solvers Through the Lens of
Adversarial Robustness [68.97830259849086]
ほとんどのデータセットは単純なサブプロブレムのみをキャプチャし、おそらくは突発的な特徴に悩まされる。
本研究では, 局所的な一般化特性である対向ロバスト性について検討し, 厳密でモデル固有な例と突発的な特徴を明らかにする。
他のアプリケーションとは異なり、摂動モデルは知覚できないという主観的な概念に基づいて設計されているため、摂動モデルは効率的かつ健全である。
驚くべきことに、そのような摂動によって、十分に表現力のあるニューラルソルバは、教師あり学習で共通する正確さと悪質さのトレードオフの限界に悩まされない。
論文 参考訳（メタデータ） (2021-10-21T07:28:11Z) - Distributionally Robust Semi-Supervised Learning Over Graphs [68.29280230284712]
グラフ構造化データに対する半教師付き学習(SSL)は、多くのネットワークサイエンスアプリケーションに現れる。
グラフ上の学習を効率的に管理するために,近年,グラフニューラルネットワーク(GNN)の変種が開発されている。
実際に成功したにも拘わらず、既存の手法のほとんどは、不確実な結節属性を持つグラフを扱うことができない。
ノイズ測定によって得られたデータに関連する分布の不確実性によっても問題が発生する。
分散ロバストな学習フレームワークを開発し,摂動に対する定量的ロバスト性を示すモデルを訓練する。
論文 参考訳（メタデータ） (2021-10-20T14:23:54Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳（メタデータ） (2021-07-15T04:47:35Z) - Computational Barriers to Estimation from Low-Degree Polynomials [81.67886161671379]
本研究では,隠れ構造物の存在を検知する作業において,低次構造物のパワーについて検討する。
大規模な「信号+雑音」問題に対して、任意の程度に達成可能な最良の平均二乗誤差に対して、ユーザフレンドリな下界を与える。
応用として,植込みサブマトリクスに対する低次平均2乗誤差の厳密な評価と高密度サブグラフ問題について述べる。
論文 参考訳（メタデータ） (2020-08-05T17:52:10Z) - Enhancing SAT solvers with glue variable predictions [2.635832975589208]
我々は、最先端のSATソルバであるCaDiCaLを改良し、SATCOMP 2018とSATRACE 2019のパフォーマンスを改善し、教師付き学習と強化学習によるSHA-1プレイメージアタックのデータセット上でのパフォーマンスを向上する。
我々はこれらの制限に対処し、より単純なネットワークアーキテクチャを用いて、数百万の節を含む大規模産業問題に対してCPU推論を行い、代わりにエミュレート変数を予測する訓練を行い、ラベル付きデータを簡単に生成し、強化学習タスクとして定式化することができる。
論文 参考訳（メタデータ） (2020-07-06T07:16:49Z) - Towards an Efficient and General Framework of Robust Training for Graph
Neural Networks [96.93500886136532]
グラフニューラルネットワーク(GNN)は、いくつかの基本的な推論タスクに大きく進歩している。
GNNの目覚ましい性能にもかかわらず、グラフ構造上の摂動を慎重に作り、誤った予測を下すことが観察されている。
我々は,強靭なGNNを得るために,欲求探索アルゴリズムとゼロ階法を利用する汎用フレームワークを提案する。
論文 参考訳（メタデータ） (2020-02-25T15:17:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。