論文の概要: Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis

• arxiv url: http://arxiv.org/abs/2107.07116v1
• Date: Thu, 15 Jul 2021 04:47:35 GMT
• ステータス: 処理完了
• システム内更新日: 2021-07-16 14:07:30.262250
• Title: Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis
• Title（参考訳）: 高速SATソルバのためのトランスフォーマーベース機械学習と論理合成
• Authors: Feng Shi, Chonghan Lee, Mohammad Khairul Bashar, Nikhil Shukla, Song-Chun Zhu and Vijaykrishnan Narayanan
• Abstract要約: CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
• 参考スコア（独自算出の注目度）: 63.53283025435107
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. The increasing popularity of these constraint problems in electronic design automation encourages studies on different SAT problems and their properties for further computational efficiency. There has been both theoretical and practical success of modern Conflict-driven clause learning SAT solvers, which allows solving very large industrial instances in a relatively short amount of time. Recently, machine learning approaches provide a new dimension to solving this challenging problem. Neural symbolic models could serve as generic solvers that can be specialized for specific domains based on data without any changes to the structure of the model. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem, which is the optimization version of SAT where the goal is to satisfy the maximum number of clauses. Our model has a scale-free structure which could process varying size of instances. We use meta-path and self-attention mechanism to capture interactions among homogeneous nodes. We adopt cross-attention mechanisms on the bipartite graph to capture interactions among heterogeneous nodes. We further apply an iterative algorithm to our model to satisfy additional clauses, enabling a solution approaching that of an exact-SAT problem. The attention mechanisms leverage the parallelism for speedup. Our evaluation indicates improved speedup compared to heuristic approaches and improved completion rate compared to machine learning approaches.
• Abstract（参考訳）: CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 電子設計自動化におけるこれらの制約問題の普及は、様々なSAT問題とその特性の研究を奨励し、さらなる計算効率を高める。 現代のコンフリクト駆動の節学習satソルバは理論的にも実用的にも成功しており、比較的短時間で非常に大きな産業インスタンスを解決できる。 最近、機械学習のアプローチは、この難しい問題を解決する新しい次元を提供する。 ニューラルシンボリックモデルは、モデルの構造を変更することなく、データに基づいて特定のドメインに特化できる汎用的なソルバとして機能する。 本研究では,最大節数を満たすことを目的としたSATの最適化版であるMaxSAT問題を解決するために,Transformerアーキテクチャから派生したワンショットモデルを提案する。 モデルにはスケールフリーな構造があり、さまざまなインスタンスのサイズを処理できます。 同種ノード間の相互作用を捉えるためにメタパスと自己認識機構を用いる。 我々は,異種ノード間の相互作用を捉えるために,二部グラフ上のクロスアテンション機構を採用する。 さらに、追加の節を満たすために反復アルゴリズムをモデルに適用し、正確なSAT問題にアプローチする解を可能にする。 注意機構は並列性を利用してスピードアップを行う。 本評価は,ヒューリスティックアプローチと比較して高速化され,機械学習アプローチに比べて完成率も向上したことを示す。

関連論文リスト

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。 これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。 私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
  論文  参考訳（メタデータ） (2024-10-18T22:25:54Z)
• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。 我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。 生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
  論文  参考訳（メタデータ） (2024-05-17T18:00:50Z)
• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  最大満足度問題(MaxSAT)の解を近似できる単一の微分可能関数を導出する。 我々は,我々の微分可能な関数をモデル化する新しいニューラルネットワークアーキテクチャを提案し,バックプロパゲーションを用いてMaxSATを段階的に解く。
  論文  参考訳（メタデータ） (2024-02-06T02:33:00Z)
• CORE: Common Random Reconstruction for Distributed Optimization with Provable Low Communication Complexity [110.50364486645852]
  コミュニケーションの複雑さは、トレーニングをスピードアップし、マシン番号をスケールアップする上で、大きなボトルネックになっています。 本稿では,機械間で送信される情報を圧縮するための共通Om REOmを提案する。
  論文  参考訳（メタデータ） (2023-09-23T08:45:27Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。 大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。 我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
  論文  参考訳（メタデータ） (2023-07-18T10:46:28Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。 これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。 本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
  論文  参考訳（メタデータ） (2022-11-16T18:59:54Z)
• A Stable, Fast, and Fully Automatic Learning Algorithm for Predictive Coding Networks [65.34977803841007]
  予測符号化ネットワークは、ベイズ統計学と神経科学の両方にルーツを持つ神経科学にインスパイアされたモデルである。 シナプス重みに対する更新規則の時間的スケジュールを変更するだけで、元の規則よりもずっと効率的で安定したアルゴリズムが得られることを示す。
  論文  参考訳（メタデータ） (2022-11-16T00:11:04Z)
• DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
  We present DeepSAT, a novel-to-end learning framework for the Boolean satisfiability (SAT) problem。 DeepSATは最先端の学習ベースSATソリューションに対して,大幅な精度向上を実現している。
  論文  参考訳（メタデータ） (2022-05-27T03:20:42Z)
• 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)

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

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