論文の概要: SATformer: Transformers for SAT Solving

• arxiv url: http://arxiv.org/abs/2209.00953v1
• Date: Fri, 2 Sep 2022 11:17:39 GMT
• ステータス: 処理完了
• システム内更新日: 2022-09-05 12:15:11.973628
• Title: SATformer: Transformers for SAT Solving
• Title（参考訳）: SATformer:SATソルビング用トランスフォーマー
• Authors: Zhengyuan Shi, Min Li, Sadaf Khan, Hui-Ling Zhen, Mingxuan Yuan, Qiang Xu
• Abstract要約: 本稿では,SAT 問題解決のためのトランスフォーマーベースの新しいソリューション SATformer を提案する。 SATformerは、不満足な問題インスタンスの最小不満足なコア(MUC)を学習する。 実験の結果,SATformerは既存のエンドツーエンド学習型SATソルバよりも強力であることがわかった。
• 参考スコア（独自算出の注目度）: 11.009299890216557
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In this paper, we propose SATformer, a novel Transformer-based solution for Boolean satisfiability (SAT) solving. Different from existing learning-based SAT solvers that learn at the problem instance level, SATformer learns the minimum unsatisfiable cores (MUC) of unsatisfiable problem instances, which provide rich information for the causality of such problems. Specifically, we apply a graph neural network (GNN) to obtain the embeddings of the clauses in the conjunctive normal format (CNF). A hierarchical Transformer architecture is applied on the clause embeddings to capture the relationships among clauses, and the self-attention weight is learned to be high when those clauses forming UNSAT cores are attended together, and set to be low otherwise. By doing so, SATformer effectively learns the correlations among clauses for SAT prediction. Experimental results show that SATformer is more powerful than existing end-to-end learning-based SAT solvers.
• Abstract（参考訳）: 本稿では,ブール充足性(SAT)解決のためのトランスフォーマーベースの新しいソリューションSATformerを提案する。 SATformerは、既存の学習ベースのSATソルバと異なり、不満足な問題インスタンスの最小不満足コア(MUC)を学習し、そのような問題の因果関係について豊富な情報を提供する。 具体的には、グラフニューラルネットワーク(GNN)を用いて、接続正規形式(CNF)における節の埋め込みを求める。 節間の関係を捉えるために、節の埋め込みに階層的トランスフォーマーアーキテクチャを適用し、UNSATコアを形成する節を一緒に参加させたときに自己注意重みを高くし、それ以外は低く設定する。 これによりSATformerはSAT予測のための節間の相関を効果的に学習する。 実験の結果,SATformerは既存のエンドツーエンド学習型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)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  分解硬度(d硬度)の概念を導入する。 d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
  論文  参考訳（メタデータ） (2023-12-16T12:44:36Z)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  本稿では,3SAT問題を解くためのハイブリッド量子コンピューティング戦略について述べる。 この近似の性能は、量子コンピューティングの観点から3-SATを扱う際に、一連の代表的なシナリオで検証されている。
  論文  参考訳（メタデータ） (2023-06-07T12:19:22Z)
• Evolutionary Diversity Optimisation in Constructing Satisfying Assignments [20.386139395296215]
  本稿では,EDOの文脈におけるブール充足可能性問題(SAT)について検討する。 SATは計算機科学において非常に重要であり、KPやTSPといったEDO文献で研究されている他の問題とは異なる。 本稿では,SAT解の集合間の多様性を明示的に最大化するために,よく知られたSATソルバを用いた進化的アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2023-05-19T06:26:10Z)
• Addressing Variable Dependency in GNN-based SAT Solving [19.38746341365531]
  本稿では、繰り返しニューラルネットワークを統合したGNNベースのアーキテクチャであるAsymSATを提案し、可変代入に対する依存予測を生成する。 実験結果から,大規模テストセット上でのSATインスタンスの解数を改善することにより,依存変数予測がGNN方式の解解能力を拡張できることが示唆された。
  論文  参考訳（メタデータ） (2023-04-18T05:33:33Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。 そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
  論文  参考訳（メタデータ） (2022-10-04T09:19:13Z)
• A Neural Network-based SAT-Resilient Obfuscation Towards Enhanced Logic Locking [3.076761061950216]
  本稿では,ニューラルネットワークを用いた unSAT 節変換器 SATConda を提案する。 SATCondaは最小限の領域と電力オーバーヘッドを発生させ、元の機能を不必要なセキュリティで保存する。 SATCondaをISCAS85およびISCAS89ベンチマークで評価した。
  論文  参考訳（メタデータ） (2022-09-13T07:59:27Z)
• 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)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)

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

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