論文の概要: 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は有望な枠組みであり、将来さらなる調査を望む新たな研究のラインを開く。
関連論文リスト
- IGMaxHS -- An Incremental MaxSAT Solver with Support for XOR Clauses [0.0]
IGMaxHS は iMaxHS と GaussMaxHS をベースとしているが, XOR の制約は GaussMaxHS よりも少ない。
IGMaxHSは、不正な不満足な判断も、不正なモデルも、一貫性のないコストモデルの組み合わせも報告していない唯一の解決法である。
IGMaxHSは,ミュンヘン量子ツールキットを用いたシミュレーションにより,量子カラーコードを復号化可能であることを示す。
論文 参考訳(メタデータ) (2024-10-21T11:21:21Z) - LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
このフレームワークはMonte Carlo Tree Search (MCTS)と反復的なSelf-Refineを組み合わせて推論パスを最適化する。
このフレームワークは、一般的なベンチマークと高度なベンチマークでテストされており、探索効率と問題解決能力の点で優れた性能を示している。
論文 参考訳(メタデータ) (2024-10-03T18:12:29Z) - Sum-of-Squares inspired Quantum Metaheuristic for Polynomial Optimization with the Hadamard Test and Approximate Amplitude Constraints [76.53316706600717]
最近提案された量子アルゴリズムarXiv:2206.14999は半定値プログラミング(SDP)に基づいている
SDPにインスパイアされた量子アルゴリズムを2乗和に一般化する。
この結果から,本アルゴリズムは大きな問題に適応し,最もよく知られた古典学に近似することが示唆された。
論文 参考訳(メタデータ) (2024-08-14T19:04:13Z) - Certified MaxSAT Preprocessing [9.717669529984349]
MaxSATはNP-hard最適化問題の解決に有効なアプローチとなっている。
MaxSATソルバの正確性を保証することは、依然として重要な関心事である。
そこで本研究では,最新のMaxSATプリプロセッシング手法の正当性を証明するために,擬似ブール検定ロギングをどのように利用できるかを示す。
論文 参考訳(メタデータ) (2024-04-26T10:55:06Z) - 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) - 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) - Fault Tree Analysis: Identifying Maximum Probability Minimal Cut Sets
with MaxSAT [0.342658286826597]
我々は,MPMCS問題を重み付き部分最大SAT問題としてモデル化し,並列SAT解決アーキテクチャを用いて解決する。
オープンソースツールで得られた結果は,このアプローチが効率的かつ効率的であることを示唆している。
論文 参考訳(メタデータ) (2020-05-05T19:47:15Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。