論文の概要: An Exact Solver for Satisfiability Modulo Counting with Probabilistic Circuits

• arxiv url: http://arxiv.org/abs/2503.01009v1
• Date: Sun, 02 Mar 2025 20:28:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-05 19:16:03.278662
• Title: An Exact Solver for Satisfiability Modulo Counting with Probabilistic Circuits
• Title（参考訳）: 確率回路を用いた満足度モードの厳密解法
• Authors: Jinzhao Li, Nan Jiang, Yexiang Xue,
• Abstract要約: SMC (Satifiability Modulo Counting) は、最近提案された一般言語である。 我々は,確率的推論プロセスにおいて,下界と上界を効率的に追跡する正確なSMC解法であるKOCO-SMCを提案する。
• 参考スコア（独自算出の注目度）: 16.645967034009225
• License:
• Abstract: Satisfiability Modulo Counting (SMC) is a recently proposed general language to reason about problems integrating statistical and symbolic artificial intelligence. An SMC formula is an extended SAT formula in which the truth values of a few Boolean variables are determined by probabilistic inference. Existing approximate solvers optimize surrogate objectives, which lack formal guarantees. Current exact solvers directly integrate SAT solvers and probabilistic inference solvers resulting in slow performance because of many back-and-forth invocations of both solvers. We propose KOCO-SMC, an integrated exact SMC solver that efficiently tracks lower and upper bounds in the probabilistic inference process. It enhances computational efficiency by enabling early estimation of probabilistic inference using only partial variable assignments, whereas existing methods require full variable assignments. In the experiment, we compare KOCO-SMC with currently available approximate and exact SMC solvers on large-scale datasets and real-world applications. Our approach delivers high-quality solutions with high efficiency.
• Abstract（参考訳）: Satisfiability Modulo Counting (SMC) は、統計的および象徴的な人工知能を統合する問題について推論するための、最近提案された汎用言語である。 SMC式(SMC formula)は、いくつかのブール変数の真理値が確率的推論によって決定される拡張SAT式である。 既存の近似解法は、正式な保証を欠いた代理目的を最適化する。 現在の正確なソルバはSATソルバと確率論的推論ソルバを直接統合しており、両者のバック・フォー・フォースな呼び出しが多いため性能が遅い。 我々は,確率的推論プロセスにおいて,下界と上界を効率的に追跡する正確なSMC解法であるKOCO-SMCを提案する。 従来の手法では完全な変数代入を必要とするのに対して、部分変数代入のみを用いて確率的推論の早期推定を可能にすることにより、計算効率を向上させる。 実験では,KOCO-SMCと現在利用可能な近似および高精度のSMCソルバを,大規模データセットや実世界のアプリケーションで比較した。 我々のアプローチは高い効率で高品質なソリューションを提供する。

関連論文リスト

• 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)
• Online POMDP Planning with Anytime Deterministic Guarantees [11.157761902108692]
  不確実性の下での計画は、部分的に観測可能なマルコフ決定プロセス(POMDP)を用いて数学的に定式化できる POMDPの最適計画を見つけるには計算コストがかかり、小さなタスクにのみ適用可能である。 簡便な解と理論的に最適な解との決定論的関係を導出する。
  論文  参考訳（メタデータ） (2023-10-03T04:40:38Z)
• Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees [18.7083987727973]
  満足度モデュロカウント(Satifiability Modulo Counting、SMC)は、象徴的な意思決定と統計的推論の両方を必要とする問題を包含する。 XOR-SMCは、SMCで数えられるモデルをSAT式に置き換えることで、非常に難解なSMCを満足できる問題に変換する。 XOR-SMC は真の最適値に近い解を見つけ、SMC における難解なモデルカウントのよい近似を見つけるのに苦戦するいくつかの基本値を上回る。
  論文  参考訳（メタデータ） (2023-09-16T05:34:59Z)
• Bayesian Quantum State Tomography with Python's PyMC [0.0]
  我々は,Python-3 のオープンソース PyMC 確率型プログラミングパッケージを用いて,複雑でない QST 最適化問題を単純な形式に変換する方法を示す。 我々は,Python-3 のオープンソース PyMC 確率型プログラミングパッケージを用いて,複雑でない QST 最適化問題を単純な形式に変換する方法を示す。
  論文  参考訳（メタデータ） (2022-12-20T21:16:28Z)
• Asymptotically Unbiased Instance-wise Regularized Partial AUC Optimization: Theory and Algorithm [101.44676036551537]
  One-way partial AUC (OPAUC) と Two-way partial AUC (TPAUC) はバイナリ分類器の平均性能を測定する。 既存の手法のほとんどはPAUCをほぼ最適化するしかなく、制御不能なバイアスにつながる。 本稿では,分散ロバスト最適化AUCによるPAUC問題の簡易化について述べる。
  論文  参考訳（メタデータ） (2022-10-08T08:26:22Z)
• 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)
• ML Supported Predictions for SAT Solvers Performance [0.0]
  内部のソルバランタイムパラメータが収集され、分析されている。 問題解決者の終了動作のバイナリ分類のための機械学習モデルが作成されている。
  論文  参考訳（メタデータ） (2021-12-17T11:17:29Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Efficient semidefinite-programming-based inference for binary and multi-class MRFs [83.09715052229782]
  分割関数やMAP推定をペアワイズMRFで効率的に計算する手法を提案する。 一般のバイナリMRFから完全多クラス設定への半定緩和を拡張し、解法を用いて再び効率的に解けるようなコンパクトな半定緩和を開発する。
  論文  参考訳（メタデータ） (2020-12-04T15:36:29Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  本稿では,学習者が生成モデルにアクセスできる場合の,割引マルコフ決定(MDP)における最良の政治的識別の問題について検討する。 最先端アルゴリズムの利点を論じ、解説する。
  論文  参考訳（メタデータ） (2020-09-28T15:22:24Z)

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

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