論文の概要: General Method for Solving Four Types of SAT Problems
- arxiv url: http://arxiv.org/abs/2312.16423v1
- Date: Wed, 27 Dec 2023 06:09:48 GMT
- ステータス: 処理完了
- システム内更新日: 2023-12-29 19:42:18.728851
- Title: General Method for Solving Four Types of SAT Problems
- Title(参考訳): 4種類のSAT問題の解法
- Authors: Anqi Li and Congying Han and Tiande Guo and Haoran Li and Bonan Li
- Abstract要約: 既存の方法は、様々なタイプのブール適合性問題(SAT)に対して様々なアルゴリズムを提供する。
本研究では,整数計画法と強化学習法(RL)に基づく統合フレームワークDCSATを提案する。
- 参考スコア(独自算出の注目度): 12.28597116379225
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: Existing methods provide varying algorithms for different types of Boolean
satisfiability problems (SAT), lacking a general solution framework.
Accordingly, this study proposes a unified framework DCSAT based on integer
programming and reinforcement learning (RL) algorithm to solve different types
of SAT problems such as MaxSAT, Weighted MaxSAT, PMS, WPMS. Specifically, we
first construct a consolidated integer programming representation for four
types of SAT problems by adjusting objective function coefficients. Secondly,
we construct an appropriate reinforcement learning models based on the 0-1
integer programming for SAT problems. Based on the binary tree search
structure, we apply the Monte Carlo tree search (MCTS) method on SAT problems.
Finally, we prove that this method can find all optimal Boolean assignments
based on Wiener-khinchin law of large Numbers. We experimentally verify that
this paradigm can prune the unnecessary search space to find the optimal
Boolean assignments for the problem. Furthermore, the proposed method can
provide diverse labels for supervised learning methods for SAT problems.
- Abstract(参考訳): 既存の手法は、様々なタイプのBoolean satisfiability problem (SAT) に対して様々なアルゴリズムを提供する。
そこで本研究では,整数プログラミングと強化学習(RL)に基づく統合フレームワーク DCSAT を提案し,MaxSAT,Weighted MaxSAT,PMS,WPMS などのSAT問題を解く。
具体的には,目的関数係数を調整して4種類のsat問題に対する統合整数計画表現を構築した。
次に,sat問題に対する0-1整数計画に基づいて,適切な強化学習モデルを構築する。
二元木探索構造に基づき,sat問題に対してモンテカルロ木探索 (mcts) 法を適用した。
最後に、この手法は、大数のWiener-khinchin法則に基づく全ての最適ブール代入を見つけることができることを示す。
このパラダイムが不必要な探索空間を創り出し、問題に対する最適なブール代入を見つけることを実験的に検証する。
さらに,SAT問題に対する教師付き学習のための多種多様なラベルを提供することができる。
関連論文リスト
- Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。
これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。
私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
論文 参考訳(メタデータ) (2024-10-18T22:25:54Z) - Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
より大規模な問題をより小さなサブコンポーネントに繰り返し分解する,Max-SATのインスタンスに対するリソース制約を提案する。
本研究では,所定のSATインスタンスの構造を利用するグラフベースの新しい手法を含む,変数選択手法の集合を分析する。
我々は,Max-SAT評価ベンチマークを用いて,ランダムに生成されたMax-SATインスタンスと実世界の実例について実験を行った。
論文 参考訳(メタデータ) (2024-10-11T18:20:08Z) - Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
分解硬度(d硬度)の概念を導入する。
d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
論文 参考訳(メタデータ) (2023-12-16T12:44:36Z) - 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) - Evolutionary Diversity Optimisation in Constructing Satisfying
Assignments [20.386139395296215]
本稿では,EDOの文脈におけるブール充足可能性問題(SAT)について検討する。
SATは計算機科学において非常に重要であり、KPやTSPといったEDO文献で研究されている他の問題とは異なる。
本稿では,SAT解の集合間の多様性を明示的に最大化するために,よく知られたSATソルバを用いた進化的アルゴリズムを提案する。
論文 参考訳(メタデータ) (2023-05-19T06:26:10Z) - 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) - 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) - Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
我々は,数千の候補アルゴリズムの固定セットを考慮に入れた,極端なアルゴリズム選択(XAS)の設定を提案する。
我々は、XAS設定に対する最先端のAS技術の適用性を評価し、Dyadic特徴表現を利用したアプローチを提案する。
論文 参考訳(メタデータ) (2020-01-29T09:40:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。