論文の概要: HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline

• arxiv url: http://arxiv.org/abs/2302.02104v3
• Date: Thu, 8 Feb 2024 13:49:57 GMT
• ステータス: 処理完了
• システム内更新日: 2024-02-09 20:01:19.617075
• 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生成アプローチでは、グローバルな構造特性を同時に捉えることはほとんどできず、高い計算硬度を維持することができる。 本稿では,SAT式生成のためのニューラル・スプリット・マージ・パラダイムに,きめ細かい制御機構を導入するHardSATGENを提案する。 従来の手法と比較すると、平均的な性能向上は構造統計の38.5%、計算の88.4%、解法チューニングの有効性の140.7%以上を達成している。
• 参考スコア（独自算出の注目度）: 45.91245228386502
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Industrial SAT formula generation is a critical yet challenging task. Existing SAT generation approaches can hardly simultaneously capture the global structural properties and maintain plausible computational hardness. 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. Experiments including evaluations on private and practical corporate testbed show the superiority of HardSATGEN being the only method to successfully augment formulae maintaining similar computational hardness and capturing the global structural properties simultaneously. Compared to the best previous methods, 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 tuning by our generated instances. Source code is available at http://github.com/Thinklab-SJTU/HardSATGEN
• Abstract（参考訳）: 産業SAT公式生成は重要な課題である。 既存のsat生成手法では、グローバルな構造特性をほぼ同時に捉えることができ、計算の難しさを維持できる。 まず,従来の学習方法の限界を深く分析し,その場合の計算の難しさを再現する手法を提案する。 産業用公式が明らかなコミュニティ構造と過分な部分構造を示すことから,論理構造のセマンティックな形成が困難であることを示す上で,SAT式生成のためのニューラルスプリット・マージ・パラダイムにきめ細かな制御機構を導入し,産業用ベンチマークの構造的・計算的特性をよりよく回復させるHardSATGENを提案する。 民間および実用的な企業試験場における評価を含む実験は、同様の計算硬さの維持とグローバルな構造特性の同時捕捉を成功させる唯一の方法であるハードサトゲンの優位性を示している。 これまでの最良の方法と比較すると、平均パフォーマンス向上率は構造統計で38.5%、計算メトリクスで88.4%、生成したインスタンスでソルバチューニングを導く効果で140.7%を超えている。 ソースコードはhttp://github.com/thinklab-sjtu/hardsatgenで利用可能

関連論文リスト

• 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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。