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

• arxiv url: http://arxiv.org/abs/2402.10705v3
• Date: Wed, 13 Nov 2024 15:46:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-14 19:24:59.466686
• Title: AutoSAT: Automatically Optimize SAT Solvers via Large Language Models
• Title（参考訳）: AutoSAT: 大規模言語モデルによるSATソルバーの自動最適化
• Authors: Yiwen Sun, Furong Ye, Xianyin Zhang, Shiyu Huang, Bingzhen Zhang, Ke Wei, Shaowei Cai,
• Abstract要約: 本稿では,既存のCDCLソルバをベースとしたモジュール型検索空間の自動最適化フレームワークであるAutoSATを提案する。 AutoSATは12データセット中9データセットでMiniSatを上回り、4データセットで最先端のハイブリッドソルバKissatを上回ります。
• 参考スコア（独自算出の注目度）: 10.359005620433136
• License:
• Abstract: Conflict-Driven Clause Learning (CDCL) is the mainstream framework for solving the Satisfiability problem (SAT), and CDCL solvers typically rely on various heuristics, which have a significant impact on their performance. Modern CDCL solvers, such as MiniSat and Kissat, commonly incorporate several heuristics and select one to use according to simple rules, requiring significant time and expert effort to fine-tune in practice. The pervasion of Large Language Models (LLMs) provides a potential solution to address this issue. However, generating a CDCL solver from scratch is not effective due to the complexity and context volume of SAT solvers. Instead, we propose AutoSAT, a framework that automatically optimizes heuristics in a pre-defined modular search space based on existing CDCL solvers. Unlike existing automated algorithm design approaches focusing on hyperparameter tuning and operator selection, AutoSAT can generate new efficient heuristics. In this first attempt at optimizing SAT solvers using LLMs, several strategies including the greedy hill climber and (1+1) Evolutionary Algorithm are employed to guide LLMs to search for better heuristics. Experimental results demonstrate that LLMs can generally enhance the performance of CDCL solvers. A realization of AutoSAT outperforms MiniSat on 9 out of 12 datasets and even surpasses the state-of-the-art hybrid solver Kissat on 4 datasets.
• Abstract（参考訳）: 競合駆動クローズラーニング(CDCL)は、 Satisfiability problem (SAT) を解くための主流フレームワークであり、CDCLソルバは通常、様々なヒューリスティックに依存しており、そのパフォーマンスに大きな影響を与えている。 ミニサット (MiniSat) やキサート (Kissat) のような現代のCDCLソルバは、一般にいくつかのヒューリスティックを取り入れ、単純な規則に従って使用するものを選択する。 LLM(Large Language Models)の普及は、この問題に対処するための潜在的な解決策を提供する。 しかし、SATソルバの複雑さとコンテキストボリュームのため、スクラッチからCDCLソルバを生成することは効果的ではない。 代わりに,既存のCDCLソルバをベースとしたモジュール探索空間において,ヒューリスティックスを自動的に最適化するフレームワークであるAutoSATを提案する。 ハイパーパラメータチューニングと演算子選択に焦点を当てた既存の自動アルゴリズム設計アプローチとは異なり、AutoSATは新たな効率的なヒューリスティックを生成することができる。 LLMを用いてSATソルバを最適化する最初の試みでは、(1+1)進化的アルゴリズム(Greedy hill climber)や(1+1) Evolutionary Algorithm)などいくつかの戦略を用いて、LLMのより優れたヒューリスティックを探索する。 実験結果から,LCMはCDCLソルバの性能を高めることができることがわかった。 AutoSATは12データセット中9データセットでMiniSatを上回り、4データセットで最先端のハイブリッドソルバKissatを上回ります。

関連論文リスト

• Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
  より大規模な問題をより小さなサブコンポーネントに繰り返し分解する,Max-SATのインスタンスに対するリソース制約を提案する。 本研究では,所定のSATインスタンスの構造を利用するグラフベースの新しい手法を含む,変数選択手法の集合を分析する。 我々は,Max-SAT評価ベンチマークを用いて,ランダムに生成されたMax-SATインスタンスと実世界の実例について実験を行った。
  論文  参考訳（メタデータ） (2024-10-11T18:20:08Z)
• Navigating the Labyrinth: Evaluating and Enhancing LLMs' Ability to Reason About Search Problems [59.72548591120689]
  我々は,11種類の検索問題を含む新しいベンチマークであるSearchBenchを紹介する。 もっとも先進的なLCMでさえ、これらの問題をエンドツーエンドのテキストで解決することができないことを示す。 LLMにその問題を解決するコードを生成するように指示することは助けになるが、GPT4のパフォーマンスは11.7%向上した。
  論文  参考訳（メタデータ） (2024-06-18T00:44:58Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。 大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。 我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
  論文  参考訳（メタデータ） (2023-07-18T10:46:28Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)
• Towards Tackling MaxSAT by Combining Nested Monte Carlo with Local Search [10.70006528984961]
  UCTMAXSAT上でのアルゴリズム的バリエーションを2つ紹介する。 まず、Nested Monte Carlo Searchアルゴリズムにインスパイアされた木探索のネストは、ベンチマークのほとんどのインスタンスタイプに有効である。 第二に、SLSの静的フリップ制限を用いることで、理想的な予算はインスタンスサイズに大きく依存し、動的に設定することを提案する。
  論文  参考訳（メタデータ） (2023-02-26T03:37:26Z)
• Efficient Adversarial Contrastive Learning via Robustness-Aware Coreset Selection [59.77647907277523]
  敵対的コントラスト学習(ACL)は、高価なデータアノテーションを必要としないが、敵対的攻撃に耐える堅牢な表現を出力する。 ACLは、すべてのトレーニングデータの逆の変種を生成するのに、膨大な実行時間が必要です。 本稿では,ACLの高速化を目的としたロバストネス対応コアセット選択(RCS)手法を提案する。
  論文  参考訳（メタデータ） (2023-02-08T03:20:14Z)
• Efficient Non-Parametric Optimizer Search for Diverse Tasks [93.64739408827604]
  興味のあるタスクを直接検索できる,スケーラブルで汎用的なフレームワークを初めて提示する。 基礎となる数学表現の自然木構造に着想を得て、空間を超木に再配置する。 我々は,モンテカルロ法を木探索に適用し,レジェクションサンプリングと等価形状検出を備える。
  論文  参考訳（メタデータ） (2022-09-27T17:51:31Z)
• New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization [0.0]
  本稿では,多目的組合せ最適化のための2つの新しい不満足性に基づくアルゴリズムを提案する。 1つはコア誘導MOCOソルバ、もう1つはヒットセットベースのMOCOソルバである。 実験の結果,新しい不満足性に基づくアルゴリズムは,MOCOの最先端SATベースのアルゴリズムより優れていることがわかった。
  論文  参考訳（メタデータ） (2022-04-22T09:46:44Z)
• 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)

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

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