論文の概要: AutoSAT: Automatically Optimize SAT Solvers via Large Language Models
- arxiv url: http://arxiv.org/abs/2402.10705v1
- Date: Fri, 16 Feb 2024 14:04:56 GMT
- ステータス: 処理完了
- システム内更新日: 2024-02-19 16:04:36.782827
- Title: AutoSAT: Automatically Optimize SAT Solvers via Large Language Models
- Title(参考訳): AutoSAT: 大規模言語モデルによるSATソルバーの自動最適化
- Authors: Yiwen Sun, Xianyin Zhang, Shiyu Huang, Shaowei Cai, Bing-Zhen Zhang,
Ke Wei
- Abstract要約: 本稿では,SATソルバの自動最適化のための新しいフレームワークであるAutoSATを紹介する。
AutoSATはLarge Large Models (LLMs)をベースにしており、コードを生成し、評価を行い、フィードバックを利用してソルバをさらに最適化することができる。
AutoSATはプラグイン・アンド・プレイベースで動作するため、大規模な予備設定やモデルトレーニングは不要である。
- 参考スコア(独自算出の注目度): 11.526994073302888
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Heuristics are crucial in SAT solvers, while no heuristic rules are suitable
for all problem instances. Therefore, it typically requires to refine specific
solvers for specific problem instances. In this context, we present AutoSAT, a
novel framework for automatically optimizing heuristics in SAT solvers. AutoSAT
is based on Large Large Models (LLMs) which is able to autonomously generate
code, conduct evaluation, then utilize the 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 preliminary setup and model training, and fosters a Chain of
Thought collaborative process with fault-tolerance, ensuring robust heuristic
optimization. Extensive experiments on a Conflict-Driven Clause Learning (CDCL)
solver demonstrates the overall superior performance of AutoSAT, especially in
solving some specific SAT problem instances.
- Abstract(参考訳): SATソルバではヒューリスティックが重要であり、すべての問題インスタンスにヒューリスティックなルールは適合しない。
したがって、通常は特定の問題インスタンスの特定のソルバを洗練する必要がある。
本稿では,SATソルバのヒューリスティックスを自動的に最適化する新しいフレームワークであるAutoSATを紹介する。
AutoSATはLarge Large Models(LLM)をベースにしており、コードを生成し、評価を行い、フィードバックを利用してヒューリスティックスをさらに最適化し、人間の介入を減らし、解決能力を向上させる。
AutoSATはプラグイン・アンド・プレイベースで動作し、広範な予備設定やモデルトレーニングの必要性を排除し、フォールトトレランスを備えたChain of Thoughtの共同プロセスを促進し、堅牢なヒューリスティックな最適化を保証する。
CDCL(Conflict-Driven Clause Learning)ソルバに関する大規模な実験は、特に特定のSAT問題インスタンスの解決において、AutoSATの全体的な優れたパフォーマンスを示す。
関連論文リスト
- 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) - Optimizing Wireless Systems Using Unsupervised and
Reinforced-Unsupervised Deep Learning [96.01176486957226]
無線ネットワークにおけるリソース割り当てとトランシーバーは、通常最適化問題の解決によって設計される。
本稿では,変数最適化と関数最適化の両問題を解くための教師なし・教師なし学習フレームワークを紹介する。
論文 参考訳(メタデータ) (2020-01-03T11:01:52Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。