論文の概要: DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving
- arxiv url: http://arxiv.org/abs/2205.03747v2
- Date: Sun, 7 May 2023 02:52:07 GMT
- ステータス: 処理完了
- システム内更新日: 2023-05-10 01:04:41.957030
- Title: DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving
- Title(参考訳): DPMS: 一般化MaxSAT解法におけるADDに基づくシンボリックアプローチ
- Authors: Anastasios Kyrillidis, Moshe Y. Vardi, Zhiwei Zhang
- Abstract要約: 本稿では,ハイブリッド制約を用いた一般化MaxSAT問題の解法について,新しい動的プログラミング手法を提案する。
我々の汎用フレームワークは、MaxSAT、Min-MaxSAT、MinSATといったCNF-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 1) (non-CNF) hybrid
constraints, such as XORs and 2) generalized MaxSAT problems natively. To
address this issue, we propose a novel dynamic-programming approach for solving
generalized MaxSAT problems with hybrid constraints -- called
\emph{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 admits many generalizations
of CNF-MaxSAT, such as MaxSAT, Min-MaxSAT, and MinSAT with hybrid constraints.
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 invites more
investigation in the future.
- Abstract(参考訳): ブールマックスSATは、Min-MaxSATやMax-hybrid-SATのような一般化された定式化とともに、ブール推論の基本的な最適化問題である。
MaxSATの既存の手法は、ベンチマークをCNF形式で解くことに成功している。
しかし 対処する能力が欠如しています
1)XORなどの(非CNF)ハイブリッド制約
2) 一般化されたmaxsat問題。
この問題に対処するために,代数的決定図(ADDs)に基づいて,ハイブリッド制約付き一般化MaxSAT問題の解法として,短縮DPMS(emph{Dynamic-Programming-MaxSAT} または DPMS)を提案する。
ADDと(段階的な)プロジェクト-ジョイントツリービルダーの力により、当社の汎用フレームワークは、MaxSAT、Min-MaxSAT、MinSATといったCNF-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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。