論文の概要: Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability

• arxiv url: http://arxiv.org/abs/2501.17493v1
• Date: Wed, 29 Jan 2025 09:01:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-30 15:54:04.603640
• Title: Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability
• Title（参考訳）: 多目的最大満足度におけるパレート最適性の証明
• Authors: Christoph Jabs, Jeremias Berg, Bart Bogaerts, Matti Järvisalo,
• Abstract要約: マルチオブジェクトMaxSAT(MO-MaxSAT)最適化手法のVeriPB証明形式に基づく証明ロギングを提案する。 最先端のマルチオブジェクトMaxSATソルバにVeriPBの証明ロギングを実装することで,MO-MaxSATの証明ロギングを合理的なオーバーヘッドで拡張可能であることを実証的に示す。
• 参考スコア（独自算出の注目度）: 9.078413809849447
• License:
• Abstract: Due to the wide employment of automated reasoning in the analysis and construction of correct systems, the results reported by automated reasoning engines must be trustworthy. For Boolean satisfiability (SAT) solvers - and more recently SAT-based maximum satisfiability (MaxSAT) solvers - trustworthiness is obtained by integrating proof logging into solvers, making solvers capable of emitting machine-verifiable proofs to certify correctness of the reasoning steps performed. In this work, we enable for the first time proof logging based on the VeriPB proof format for multi-objective MaxSAT (MO-MaxSAT) optimization techniques. Although VeriPB does not offer direct support for multi-objective problems, we detail how preorders in VeriPB can be used to provide certificates for MO-MaxSAT algorithms computing a representative solution for each element in the non-dominated set of the search space under Pareto-optimality, without extending the VeriPB format or the proof checker. By implementing VeriPB proof logging into a state-of-the-art multi-objective MaxSAT solver, we show empirically that proof logging can be made scalable for MO-MaxSAT with reasonable overhead.
• Abstract（参考訳）: 自動推論が正しいシステムの解析と構築に広く採用されているため、自動推論エンジンによって報告された結果は信頼できるものでなければならない。 Boolean satisfiability(SAT)ソルバと、最近ではSATベースの最大満足度(MaxSAT)ソルバに対して、証明ロギングをソルバに統合し、機械検証可能な証明を出力し、推論ステップの正しさを証明して信頼性を得る。 本研究では,多目的MaxSAT (MO-MaxSAT) 最適化手法の VeriPB 証明形式に基づく検定ロギングを初めて実現した。 VeriPBは多目的問題を直接サポートしていないが、VeriPBフォーマットや証明チェッカーを拡張することなく、Pareto-Optimalityの下での検索空間の非支配的集合における各要素の代表的な解を計算するMO-MaxSATアルゴリズムの証明を、VeriPBのプレオーダーがどのように利用できるのかを詳述する。 最先端のマルチオブジェクトMaxSATソルバにVeriPBの証明ロギングを実装することで,MO-MaxSATの証明ロギングを合理的なオーバーヘッドで拡張可能であることを実証的に示す。

関連論文リスト

• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• 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)
• Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects [1.6727186769396274]
  満足度に基づく自動推論は、ソフトウェア工学において複雑なソフトウェアを検証するのに成功している。 我々は、FOL*不満足な結果の正しさを検証するという課題に取り組む。 我々は,不満足の原因を説明するために,証明に基づく診断法を開発した。
  論文  参考訳（メタデータ） (2024-09-13T22:25:58Z)
• Certified MaxSAT Preprocessing [9.717669529984349]
  MaxSATはNP-hard最適化問題の解決に有効なアプローチとなっている。 MaxSATソルバの正確性を保証することは、依然として重要な関心事である。 そこで本研究では,最新のMaxSATプリプロセッシング手法の正当性を証明するために,擬似ブール検定ロギングをどのように利用できるかを示す。
  論文  参考訳（メタデータ） (2024-04-26T10:55:06Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。 これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。 本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
  論文  参考訳（メタデータ） (2022-11-16T18:59:54Z)
• DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving [45.21499915442282]
  本稿では,ハイブリッド制約を用いた一般化MaxSAT問題の解法について,新しい動的プログラミング手法を提案する。 我々の汎用フレームワークは、MaxSAT、Min-MaxSAT、MinSATといったCNF-MaxSATの多くの一般化をハイブリッド制約で認めている。 実験の結果、DPMSは様々な手法に基づく他のアルゴリズムがすべて失敗し、特定の問題を迅速に解決できることがわかった。
  論文  参考訳（メタデータ） (2022-05-08T00:31:53Z)
• 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)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  本稿では,学習者が生成モデルにアクセスできる場合の,割引マルコフ決定(MDP)における最良の政治的識別の問題について検討する。 最先端アルゴリズムの利点を論じ、解説する。
  論文  参考訳（メタデータ） (2020-09-28T15:22:24Z)
• Fault Tree Analysis: Identifying Maximum Probability Minimal Cut Sets with MaxSAT [0.342658286826597]
  我々は,MPMCS問題を重み付き部分最大SAT問題としてモデル化し,並列SAT解決アーキテクチャを用いて解決する。 オープンソースツールで得られた結果は,このアプローチが効率的かつ効率的であることを示唆している。
  論文  参考訳（メタデータ） (2020-05-05T19:47:15Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。