論文の概要: Certified MaxSAT Preprocessing

• arxiv url: http://arxiv.org/abs/2404.17316v1
• Date: Fri, 26 Apr 2024 10:55:06 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-29 13:24:47.111459
• Title: Certified MaxSAT Preprocessing
• Title（参考訳）: 認証MaxSAT前処理
• Authors: Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Jakob Nordström,
• Abstract要約: MaxSATはNP-hard最適化問題の解決に有効なアプローチとなっている。 MaxSATソルバの正確性を保証することは、依然として重要な関心事である。 そこで本研究では,最新のMaxSATプリプロセッシング手法の正当性を証明するために,擬似ブール検定ロギングをどのように利用できるかを示す。
• 参考スコア（独自算出の注目度）: 9.717669529984349
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving NP-hard optimization problems, but ensuring correctness of MaxSAT solvers has remained an important concern. For SAT, this is largely a solved problem thanks to the use of proof logging, meaning that solvers emit machine-verifiable proofs of (un)satisfiability to certify correctness. However, for MaxSAT, proof logging solvers have started being developed only very recently. Moreover, these nascent efforts have only targeted the core solving process, ignoring the preprocessing phase where input problem instances can be substantially reformulated before being passed on to the solver proper. In this work, we demonstrate how pseudo-Boolean proof logging can be used to certify the correctness of a wide range of modern MaxSAT preprocessing techniques. By combining and extending the VeriPB and CakePB tools, we provide formally verified, end-to-end proof checking that the input and preprocessed output MaxSAT problem instances have the same optimal value. An extensive evaluation on applied MaxSAT benchmarks shows that our approach is feasible in practice.
• Abstract（参考訳）: 過去数十年間のブール充足可能性(SAT)解決の進展を踏まえ、最大充足可能性(MaxSAT)はNP-ハード最適化問題の解決に有効なアプローチとなっているが、MaxSATソルバの正しさの確保は依然として重要な懸念点である。 SATの場合、これは証明ロギング(英語版)を用いることにより、主に解決された問題である。 しかし、MaxSATでは、証明ロギング解決器が開発され始めたのはごく最近である。 さらに、これらの初期段階の取り組みは、コア解決プロセスのみを対象としており、入力問題インスタンスが適切な解決者に渡される前に実質的に再構成される前処理フェーズを無視している。 本研究は,最新のMaxSATプリプロセッシング技術の正確性を証明するために,疑似ブール検定ロギングがいかに有効かを示すものである。 VeriPB と CakePB のツールを組み合わせて拡張することにより,入力および前処理した MaxSAT 問題インスタンスが同じ最適値であることを確認する。 応用MaxSATベンチマークの広範な評価は、我々のアプローチが実際に実現可能であることを示している。

関連論文リスト

• Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
  より大規模な問題をより小さなサブコンポーネントに繰り返し分解する,Max-SATのインスタンスに対するリソース制約を提案する。 本研究では,所定のSATインスタンスの構造を利用するグラフベースの新しい手法を含む,変数選択手法の集合を分析する。 我々は,Max-SAT評価ベンチマークを用いて,ランダムに生成されたMax-SATインスタンスと実世界の実例について実験を行った。
  論文  参考訳（メタデータ） (2024-10-11T18:20:08Z)
• 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)
• 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)
• 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)
• 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)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。 ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。 本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
  論文  参考訳（メタデータ） (2020-10-07T08:19:48Z)
• 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)

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

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