論文の概要: DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving
- arxiv url: http://arxiv.org/abs/2205.03747v1
- Date: Sun, 8 May 2022 00:31:53 GMT
- ステータス: 処理完了
- システム内更新日: 2022-05-15 05:50:57.186496
- Title: DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving
- Title(参考訳): DPMS: 一般化MaxSAT解法におけるADDに基づくシンボリックアプローチ
- Authors: Anastasios Kyrillidis, Moshe Y. Vardi, Zhiwei Zhang
- Abstract要約: 代数的決定図(ADD)に基づく一般化MaxSAT問題の解法に関する新しい動的プログラミング手法を提案する。
我々の汎用フレームワークは、非CNF制約を持つMaxSATやMin-MaxSAT、MinSATなど、MaxSATの多くの一般化を処理できる。
実証的な結果から、DPMSは特定の問題を迅速に解き、他のアルゴリズムは全て失敗することを示している。
- 参考スコア(独自算出の注目度): 45.21499915442282
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Boolean MaxSAT, as well as generalized formulations such as Min-MaxSAT and
Max-hybrid-SAT, are fundamental optimization problems in Boolean reasoning.
Existing methods for MaxSAT have been successful in solving benchmarks in CNF
format. They lack, however, the ability to handle hybrid and generalized MaxSAT
problems natively. To address this issue, we propose a novel
dynamic-programming approach for solving generalized MaxSAT problems -- called
Dynamic-Programming-MaxSAT or DPMS for short -- based on Algebraic Decision
Diagrams (ADDs). With the power of ADDs and the (graded) project-join-tree
builder, our versatile framework can handle many generalizations of MaxSAT,
such as MaxSAT with non-CNF constraints, Min-MaxSAT and MinSAT. Moreover, DPMS
scales provably well on instances with low width. Empirical results indicate
that DPMS is able to solve certain problems quickly, where other algorithms
based on various techniques all fail. Hence, DPMS is a promising framework and
opens a new line of research that desires more investigation in the future.
- Abstract(参考訳): ブールマックスSATは、Min-MaxSATやMax-hybrid-SATのような一般化された定式化とともに、ブール推論の基本的な最適化問題である。
MaxSATの既存の手法は、ベンチマークをCNF形式で解くことに成功している。
しかし、ハイブリッドで一般化されたMaxSAT問題をネイティブに処理する能力は欠如している。
そこで本研究では,代数的決定図(ADD)に基づく,一般化されたMaxSAT問題の解法であるDynamic-Programming-MaxSATあるいはDPMSを提案する。
ADDと(段階的な)プロジェクト-ジョイントツリービルダーの力により、私たちの汎用フレームワークは、MaxSATの非CNF制約を持つMaxSATやMin-MaxSAT、MinSATなど、MaxSATの多くの一般化を処理できます。
さらに、DPMSは低い幅のインスタンスで確実にスケールする。
実験の結果、DPMSは様々な手法に基づく他のアルゴリズムがすべて失敗し、特定の問題を迅速に解決できることがわかった。
そのため、DPMSは有望な枠組みであり、将来さらなる調査を望む新たな研究のラインを開く。
関連論文リスト
- SEGO: Sequential Subgoal Optimization for Mathematical Problem-Solving [64.38649623473626]
大規模言語モデル(LLM)は人工知能の大幅な進歩を導いた。
数学的問題を解く能力を高めるために,textbfSEquential subtextbfGoal textbfOptimization (SEGO) という新しいフレームワークを提案する。
論文 参考訳(メタデータ) (2023-10-19T17:56:40Z) - UpMax: User partitioning for MaxSAT [2.2022484178680872]
パーティショニングは、不満に基づくMaxSATアルゴリズムのパフォーマンスに大きな影響を与える。
本稿では,分割処理をMaxSATの解法から切り離すUpMaxという新しいフレームワークを提案する。
論文 参考訳(メタデータ) (2023-05-25T15:50:00Z) - Decentralized Riemannian Algorithm for Nonconvex Minimax Problems [82.50374560598493]
ニューラルネットワークのためのミニマックスアルゴリズムは、多くの問題を解決するために開発された。
本稿では,2種類のミニマックスアルゴリズムを提案する。
そこで我々は, DRSGDAを提案し, 本手法が勾配を達成することを証明した。
論文 参考訳(メタデータ) (2023-02-08T01:42:45Z) - Constrained mixers for the quantum approximate optimization algorithm [55.41644538483948]
ヒルベルト空間全体の部分空間への発展を制限する混合作用素を構築するための枠組みを提案する。
我々は,「ワンホット」状態の部分空間を保存するために設計された「XY」ミキサーを,多くの計算基底状態によって与えられる部分空間の一般の場合に一般化する。
我々の分析は、現在知られているよりもCXゲートが少ない"XY"ミキサーのトロタライズも有効である。
論文 参考訳(メタデータ) (2022-03-11T17:19:26Z) - BandMaxSAT: A Local Search MaxSAT Solver with Multi-armed Bandit [16.371916145216737]
そこで我々はBandMaxSATという局所探索アルゴリズムを提案する。
広汎な実験により、BandMaxSATは最先端(W)PMS局所探索アルゴリズムSATLike3.0を大きく上回っていることが示された。
その結果、BandMaxSAT-cはSATLike-c、Loandra、TT-Open-WBO-Incなど、最先端の完全(W)PMSソルバよりも優れている。
論文 参考訳(メタデータ) (2022-01-14T16:32:39Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - Incomplete MaxSAT Approaches for Combinatorial Testing [0.0]
本稿では,最小長の制約付き混合被覆アレイを構築するためのSAT(Satifiability)に基づくアプローチを提案する。
この問題はシステム障害検出のためのコンビネータテストの中心である。
論文 参考訳(メタデータ) (2021-05-26T14:00:56Z) - On Continuous Local BDD-Based Search for Hybrid SAT Solving [40.252804008544985]
CLSに必要な勾配を効率的に計算するための新しいアルゴリズムを提案する。
多くのベンチマークインスタンスに適用することにより、多用途CLSソルバであるGradSATの機能と限界について検討する。
実験結果から,GradSATは既存のSATおよびMaxSATソルバのポートフォリオに追加され,ブール適合性および最適化問題の解決に有用であることが示唆された。
論文 参考訳(メタデータ) (2020-12-14T22:36:20Z) - Fault Tree Analysis: Identifying Maximum Probability Minimal Cut Sets
with MaxSAT [0.342658286826597]
我々は,MPMCS問題を重み付き部分最大SAT問題としてモデル化し,並列SAT解決アーキテクチャを用いて解決する。
オープンソースツールで得られた結果は,このアプローチが効率的かつ効率的であることを示唆している。
論文 参考訳(メタデータ) (2020-05-05T19:47:15Z) - Hardness of Random Optimization Problems for Boolean Circuits,
Low-Degree Polynomials, and Langevin Dynamics [78.46689176407936]
アルゴリズムの族は高い確率でほぼ最適な解を生成できないことを示す。
ブール回路の場合、回路複雑性理論で知られている最先端境界を改善する。
論文 参考訳(メタデータ) (2020-04-25T05:45:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。