論文の概要: AutoSAT: Automatically Optimize SAT Solvers via Large Language Models

• arxiv url: http://arxiv.org/abs/2402.10705v2
• Date: Fri, 31 May 2024 11:38:00 GMT
• ステータス: 処理完了
• システム内更新日: 2024-06-03 19:52:35.357492
• Title: AutoSAT: Automatically Optimize SAT Solvers via Large Language Models
• Title（参考訳）: AutoSAT: 大規模言語モデルによるSATソルバーの自動最適化
• Authors: Yiwen Sun, Xianyin Zhang, Shiyu Huang, Shaowei Cai, BingZhen Zhang, Ke Wei,
• Abstract要約: 本稿では,SATソルバの自動最適化のための新しいフレームワークであるAutoSATを紹介する。 AutoSATは、コードの自動生成が可能なLarge Language Models (LLM)に基づいている。 AutoSATはプラグイン・アンド・プレイベースで動作し、広範なエンタープライズおよびモデルトレーニングの必要性を排除している。
• 参考スコア（独自算出の注目度）: 10.87846542244079
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Heuristics are crucial in SAT solvers, but no heuristic rules are suitable for all SAT problems. Therefore, it is helpful to refine specific heuristics for specific problems. In this context, we present AutoSAT, a novel framework for automatically optimizing heuristics in SAT solvers. AutoSAT is based on Large Language Models (LLMs) which is able to autonomously generate codes, conduct evaluation, and then utilize feedback to further optimize heuristics, thereby reducing human intervention and enhancing solver capabilities. AutoSAT operates on a plug-and-play basis, eliminating the need for extensive enterprise and model training, and fosters a Multi-Agent-based collaborative process with fault tolerance to ensure robust heuristic optimization. We implement AutoSAT on a lightweight Conflict-Driven Clause Learning (CDCL) solver EasySAT (the volume of EasySAT is about one-fiftieth of the State-of-the-Art hybrid solver Kissat) and extensive experiments on seven datasets demonstrate its superior performance. Out of the seven testing datasets, AutoSAT shows a superior performance to Kissat in two datasets and displays an overall similar performance in three datasets. Some heuristics generated by AutoSAT are even counter-intuitive but are very effective.
• Abstract（参考訳）: SATソルバではヒューリスティックが重要であるが、すべてのSAT問題にはヒューリスティックなルールが適していない。 したがって、特定の問題に対する特定のヒューリスティックスを洗練させるのに役立つ。 本稿では,SATソルバのヒューリスティックスを自動的に最適化する新しいフレームワークであるAutoSATを紹介する。 AutoSATはLarge Language Models (LLMs)をベースにしており、コードを生成し、評価を行い、フィードバックを利用してヒューリスティックスをさらに最適化し、人間の介入を減らし、解決能力を向上させる。 AutoSATはプラグイン・アンド・プレイベースで動作し、広範なエンタープライズおよびモデルトレーニングの必要性を排除し、堅牢なヒューリスティック最適化を保証するために、フォールトトレランスを備えたマルチエージェントベースのコラボレーティブプロセスを促進する。 我々は、軽量な衝突駆動クロース学習(CDCL)ソルバ、EasySAT(EasySATの体積は、State-of-the-ArtハイブリッドソルバKissatの約5分の1)にAutoSATを実装し、その優れた性能を示す7つのデータセットに関する広範な実験を行った。 7つのテストデータセットのうち、AutoSATは2つのデータセットでKissatよりも優れたパフォーマンスを示し、3つのデータセットで全体的な同様のパフォーマンスを示している。 AutoSATが生成したヒューリスティックは直感に反するものもあるが、非常に効果的である。

関連論文リスト

• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  分解硬度(d硬度)の概念を導入する。 d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
  論文  参考訳（メタデータ） (2023-12-16T12:44:36Z)
• EduSAT: A Pedagogical Tool for Theory and Applications of Boolean Satisfiability [4.392308906793852]
  EduSAT は SAT と Satisfiability Modulo Theories (SMT) の学習と理解を支援するツールである。 SATとSMT以外の5つのNP完全問題に対して、鍵アルゴリズムとソルバ抽象化の実装を提供する。 EduSATの利点は、SATとSMTの問題解決技術を実験、分析、検証することで得られる。
  論文  参考訳（メタデータ） (2023-08-15T17:31:35Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。 大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。 我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
  論文  参考訳（メタデータ） (2023-07-18T10:46:28Z)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  本稿では,3SAT問題を解くためのハイブリッド量子コンピューティング戦略について述べる。 この近似の性能は、量子コンピューティングの観点から3-SATを扱う際に、一連の代表的なシナリオで検証されている。
  論文  参考訳（メタデータ） (2023-06-07T12:19:22Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)
• W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs [13.173307471333619]
  W2SATは、現実世界/産業インスタンスから固有の構造と特性を学ぶことによってSAT式を生成するフレームワークである。 Weighted Literal Incidence Graph (WLIG)と呼ばれる新しいSAT表現を導入する。 WLIGからSAT問題への復号化は、新しい丘登り最適化法で重なり合う斜角を見つけることをモデル化する。
  論文  参考訳（メタデータ） (2023-02-01T06:30:41Z)
• 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)
• SATformer: Transformer-Based UNSAT Core Learning [0.0]
  本稿では,SAT 問題に対する Transformer ベースのアプローチである SATformer を紹介する。 SATformerは、問題を直接解決するのではなく、満足できないことに焦点をあてて、その問題を反対方向からアプローチする。 SATformerは、シングルビットの満足度結果と最小限の不満コアを使用して、マルチタスク学習アプローチでトレーニングされる。 実験の結果,SATformerは既存のソルバのランタイムを平均21.33%削減できることがわかった。
  論文  参考訳（メタデータ） (2022-09-02T11:17:39Z)
• 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)

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

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