論文の概要: HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation
and A Strong Structure-Hardness-Aware Baseline
- arxiv url: http://arxiv.org/abs/2302.02104v1
- Date: Sat, 4 Feb 2023 05:58:17 GMT
- ステータス: 処理完了
- システム内更新日: 2023-02-07 20:15:01.216677
- Title: HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation
and A Strong Structure-Hardness-Aware Baseline
- Title（参考訳）: ハードサトゲン:ハードSATフォーミュラの難易度と強構造に配慮したベースラインの理解
- Authors: Yang Li, Xinyan Chen, Wenxuan Guo, Xijun Li, Wanqian Luo, Junhua
Huang, Hui-Ling Zhen, Mingxuan Yuan, Junchi Yan
- Abstract要約: 既存のSAT生成アプローチでは、グローバルな構造特性を同時に捉えることはほとんどできず、高い計算硬度を維持することができる。
本稿では,産業ベンチマークの構造的および計算的特性をよりよく回復する,きめ細かい制御機構を導入するHardSATGENを提案する。
従来の手法と比較して、平均的な性能向上は構造統計の38.5%、計算メトリクスの88.4%、および生成したインスタンスによって調整された解法開発を導く効果の140.7%以上を達成している。
- 参考スコア（独自算出の注目度）: 58.52561620622982
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Industrial SAT formula generation is a critical yet challenging task for
heuristic development and the surging learning-based methods in practical SAT
applications. Existing SAT generation approaches can hardly simultaneously
capture the global structural properties and maintain plausible computational
hardness, which can be hazardous for the various downstream engagements. To
this end, we first present an in-depth analysis for the limitation of previous
learning methods in reproducing the computational hardness of original
instances, which may stem from the inherent homogeneity in their adopted
split-merge procedure. On top of the observations that industrial formulae
exhibit clear community structure and oversplit substructures lead to the
difficulty in semantic formation of logical structures, we propose HardSATGEN,
which introduces a fine-grained control mechanism to the neural split-merge
paradigm for SAT formula generation to better recover the structural and
computational properties of the industrial benchmarks. Experimental results
including evaluations on private corporate data and hyperparameter tuning over
solvers in practical use show the significant superiority of HardSATGEN being
the only method to successfully augments formulae maintaining similar
computational hardness and capturing the global structural properties
simultaneously. Compared to the best previous methods to our best knowledge,
the average performance gains achieve 38.5% in structural statistics, 88.4% in
computational metrics, and over 140.7% in the effectiveness of guiding solver
development tuned by our generated instances.
- Abstract（参考訳）: 産業SAT公式生成は、実用SATアプリケーションにおけるヒューリスティックな開発と学習に基づく手法の急増にとって、重要かつ困難な課題である。
既存のSAT生成アプローチでは、グローバルな構造特性を同時に捉えることはほとんどできず、様々な下流のエンゲージメントにとって有害な計算硬度を維持することができる。
この目的のために,本研究では,従来の学習方法の制限について,従来の計算困難度を再現するための詳細な解析を行った。
産業用公式が明らかなコミュニティ構造と過分な部分構造を示すことから,論理構造のセマンティックな形成が困難であることを示す上で,SAT式生成のためのニューラルスプリット・マージ・パラダイムにきめ細かな制御機構を導入し,産業用ベンチマークの構造的・計算的特性をよりよく回復させるHardSATGENを提案する。
計算硬度とグローバルな構造特性の同時把握を両立させる手法として, 民間企業データの評価や, 実用化におけるハイパーパラメータチューニングなどの実験結果から, ハードサトゲンの有意な優位性が確認された。
我々の最高の知識に対する最高の手法と比較すると、平均的な性能向上は構造統計で38.5%、計算メトリクスで88.4%、生成したインスタンスでチューニングされたソルバ開発を導く効果で140.7%以上を達成している。
関連論文リスト
- The Power of Resets in Online Reinforcement Learning [73.64852266145387]
ローカルシミュレータアクセス(あるいはローカルプランニング)を用いたオンライン強化学習を通してシミュレータのパワーを探求する。
カバー性が低いMPPは,Qstar$-realizabilityのみのサンプル効率で学習可能であることを示す。
ローカルシミュレーターアクセス下では, 悪名高いExogenous Block MDP問題が抽出可能であることを示す。
論文 参考訳（メタデータ） (2024-04-23T18:09:53Z) - Using deep learning to construct stochastic local search SAT solvers
with performance bounds [0.0]
グラフニューラルネットワークを用いてオーラクルを訓練し、2つのSLSソルバ上で、様々な難易度を持つランダムSATインスタンス上でそれらを評価する。
GNNベースのオラクルへのアクセスは,両者のパフォーマンスを著しく向上させることがわかった。
論文 参考訳（メタデータ） (2023-09-20T16:27:52Z) - Structured Sentiment Analysis as Transition-based Dependency Parsing [0.40611352512781856]
構造化感情分析は、自然言語のテキストから人の意見を自動的に抽出することを目的としている。
SSAを実行するための最も正確な方法の1つが最近提案され、依存関係解析タスクとしてアプローチされている。
依存関係解析としてSSAに対処する最初の遷移ベース手法を提案する。
論文 参考訳（メタデータ） (2023-05-09T10:03:34Z) - Principled and Efficient Motif Finding for Structure Learning of Lifted
Graphical Models [5.317624228510748]
構造学習は、ニューロシンボリックAIと統計リレーショナル学習の分野の中心となるAIの中核的な問題である。
昇降型グラフィカルモデルにおける構造モチーフのマイニングのための第一原理的アプローチを提案する。
我々は,最先端構造学習の手法を,精度で最大6%,実行時の最大80%で上回ることを示す。
論文 参考訳（メタデータ） (2023-02-09T12:21:55Z) - 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) - Amortized Inference for Causal Structure Learning [72.84105256353801]
因果構造を学習することは、通常、スコアまたは独立テストを使用して構造を評価することを伴う探索問題を引き起こす。
本研究では,観測・干渉データから因果構造を予測するため,変分推論モデルを訓練する。
我々のモデルは、実質的な分布シフトの下で頑健な一般化能力を示す。
論文 参考訳（メタデータ） (2022-05-25T17:37:08Z) - Symbolic Regression by Exhaustive Search: Reducing the Search Space
Using Syntactical Constraints and Efficient Semantic Structure Deduplication [2.055204980188575]
シンボリック回帰は、モデル構造に関する事前の知識が得られない産業シナリオにおいて、強力なシステム識別技術である。
この章では、これらの問題に対処するために特別に設計された決定論的シンボリック回帰アルゴリズムを紹介します。
全ての可能なモデルの有限列挙は、構造的制約と意味論的に等価な解を検出するキャッシング機構によって保証される。
論文 参考訳（メタデータ） (2021-09-28T17:47:51Z) - RANK-NOSH: Efficient Predictor-Based Architecture Search via Non-Uniform
Successive Halving [74.61723678821049]
予算の浪費を回避するため,早期に性能の低いアーキテクチャのトレーニングを終了する階層的スケジューリングアルゴリズムであるNOn-uniform Successive Halving (NOSH)を提案する。
予測器に基づくアーキテクチャ探索をペア比較でランク付けする学習として定式化する。
その結果、RANK-NOSHは検索予算を5倍に削減し、様々な空間やデータセットにおける従来の最先端予測手法よりも、競争力やパフォーマンスの向上を実現した。
論文 参考訳（メタデータ） (2021-08-18T07:45:21Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳（メタデータ） (2021-07-15T04:47:35Z) - Efficient Micro-Structured Weight Unification and Pruning for Neural
Network Compression [56.83861738731913]
ディープニューラルネットワーク(DNN)モデルは、特にリソース制限されたデバイスにおいて、実用的なアプリケーションに不可欠である。
既往の非構造的あるいは構造化された重量刈り法は、推論を真に加速することはほとんど不可能である。
ハードウェア互換のマイクロ構造レベルでの一般化された重み統一フレームワークを提案し,高い圧縮と加速度を実現する。
論文 参考訳（メタデータ） (2021-06-15T17:22:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。