論文の概要: Synthesising Recursive Functions for First-Order Model Counting:
Challenges, Progress, and Conjectures
- arxiv url: http://arxiv.org/abs/2306.04189v1
- Date: Wed, 7 Jun 2023 06:49:01 GMT
- ステータス: 処理完了
- システム内更新日: 2023-06-08 16:00:10.060712
- Title: Synthesising Recursive Functions for First-Order Model Counting:
Challenges, Progress, and Conjectures
- Title(参考訳): 一階モデルカウントのための再帰関数の合成:挑戦,進歩,予想
- Authors: Paulius Dilkas, Vaishak Belle
- Abstract要約: 1次モデルカウント(英: First-order model counting、FOMC)は、有限領域の1次論理において文のモデルを数えるように要求する計算問題である。
私たちは、典型的にドメイン再帰に伴う制限を緩和し、サイクルを含むかもしれない有向グラフを扱う。
これらの改良により、アルゴリズムはそれまで到達範囲を超えていた問題を数えるための効率的な解を見つけることができる。
- 参考スコア(独自算出の注目度): 12.47276164048813
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: First-order model counting (FOMC) is a computational problem that asks to
count the models of a sentence in finite-domain first-order logic. In this
paper, we argue that the capabilities of FOMC algorithms to date are limited by
their inability to express many types of recursive computations. To enable such
computations, we relax the restrictions that typically accompany domain
recursion and generalise the circuits used to express a solution to an FOMC
problem to directed graphs that may contain cycles. To this end, we adapt the
most well-established (weighted) FOMC algorithm ForcLift to work with such
graphs and introduce new compilation rules that can create cycle-inducing edges
that encode recursive function calls. These improvements allow the algorithm to
find efficient solutions to counting problems that were previously beyond its
reach, including those that cannot be solved efficiently by any other exact
FOMC algorithm. We end with a few conjectures on what classes of instances
could be domain-liftable as a result.
- Abstract(参考訳): 1次モデルカウント(英: First-order model counting、FOMC)は、有限領域の1次論理において文のモデルを数えるように求める計算問題である。
本稿では,従来のFOMCアルゴリズムでは,多くの再帰的計算を表現できないため,その能力に制限があると主張している。
このような計算を可能にするために、通常、領域再帰を伴う制限を緩和し、サイクルを含む有向グラフに対してfomc問題の解を表現するのに使われる回路を一般化する。
この目的のために、最も確立された(重み付けされた)FOMCアルゴリズムであるForcLiftを、そのようなグラフを扱うように適応させ、再帰関数呼び出しをエンコードするサイクル誘導エッジを生成する新しいコンパイルルールを導入する。
これらの改良により、他のfomcアルゴリズムでは効率的に解くことができない問題を含む、それまで到達できなかった問題に対する効率的な解を見つけることができる。
結果として、どのインスタンスのクラスがドメインリフト可能かといういくつかの予想に終止符を打つ。
関連論文リスト
- Towards Practical First-Order Model Counting [25.295313268611217]
1次モデルカウント(英: First-order model counting、FOMC)とは、一階述語論理における文のモデル数をカウントする問題である。
1次知識コンパイルに基づく新しい手法が提案された。
この研究の主な貢献は、関数定義を任意の精度演算を備えたC++コードに変換するGantryと呼ばれる完全自動コンパイルアルゴリズムである。
論文 参考訳(メタデータ) (2025-02-17T19:28:06Z) - A Sample Efficient Alternating Minimization-based Algorithm For Robust Phase Retrieval [56.67706781191521]
そこで本研究では,未知の信号の復元を課題とする,ロバストな位相探索問題を提案する。
提案するオラクルは、単純な勾配ステップと外れ値を用いて、計算学的スペクトル降下を回避している。
論文 参考訳(メタデータ) (2024-09-07T06:37:23Z) - Symmetric Tensor Networks for Generative Modeling and Constrained
Combinatorial Optimization [72.41480594026815]
ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。
これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。
本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
論文 参考訳(メタデータ) (2022-11-16T18:59:54Z) - Scalable Anytime Algorithms for Learning Formulas in Linear Temporal
Logic [2.631744051718347]
トレースを分類する公式を学習する際の問題点を考察する。
既存の解には2つの制限がある: それらは小さな公式を超えてスケールせず、結果を返すことなく計算資源を消費する。
我々は,両問題に対処する新しいアルゴリズムを導入する。我々のアルゴリズムは,従来よりも桁違いに大きい式を構築でき,いつでも可能である。
論文 参考訳(メタデータ) (2021-10-13T13:57:31Z) - Strengthening Probabilistic Graphical Models: The Purge-and-merge
Algorithm [0.0]
パージ・アンド・マージアルゴリズムは、因子を選択的にマージすることで、可鍛グラフ構造を木構造に向けるように設計されている。
このアプローチは,Sudoku,Fill-a-pix,Kakuroなど,数多くの制約満足パズルに対して評価される。
これらのタスクは CSP のバイナリ論理に限られていたが、一般の PGM 推論への拡張の約束があると考えている。
論文 参考訳(メタデータ) (2021-09-30T21:20:52Z) - Dynamic programming by polymorphic semiring algebraic shortcut fusion [1.9405875431318445]
動的プログラミング(動的プログラミング、英: Dynamic Programming、DP)は、難解問題の効率的かつ正確な解法のためのアルゴリズム設計パラダイムである。
本稿では,セミリングに基づくDPアルゴリズムを体系的に導出するための厳密な代数形式について述べる。
論文 参考訳(メタデータ) (2021-07-05T00:51:02Z) - Non-approximate Inference for Collective Graphical Models on Path Graphs
via Discrete Difference of Convex Algorithm [19.987509826212115]
本稿では,パスグラフ上の集合的グラフィカルモデル(CGM)に対するMAP推論の新しい手法を提案する。
まず、MAP推論問題を(非線形)最小コストフロー問題として定式化できることを示す。
提案手法では,dcaの重要なサブルーチンを最小凸コストフローアルゴリズムにより効率的に計算できる。
論文 参考訳(メタデータ) (2021-02-18T07:28:18Z) - Boosting Data Reduction for the Maximum Weight Independent Set Problem
Using Increasing Transformations [59.84561168501493]
最大重み独立集合問題に対する新しい一般化データ削減および変換規則を導入する。
驚くべきことに、これらのいわゆる増進変換は問題を単純化し、還元空間を開き、アルゴリズムの後にさらに小さな既約グラフが得られる。
提案アルゴリズムは, 1つのインスタンスを除くすべての既約グラフを計算し, 従来よりも多くのインスタンスを最適に解き, 最高の最先端解法よりも最大2桁高速に解き, 解法DynWVCやHILSよりも高品質な解を求める。
論文 参考訳(メタデータ) (2020-08-12T08:52:50Z) - Sparsified Linear Programming for Zero-Sum Equilibrium Finding [89.30539368124025]
我々は、この問題に対して全く異なるアプローチを示し、それは競争力があり、しばしば、以前の最先端技術よりも桁違いに優れている。
ポーカーエンドゲームの実験により、現代の線形プログラムソルバは、ゲーム固有のCFRの現代的な変種でさえも競合することを示した。
論文 参考訳(メタデータ) (2020-06-05T13:48:26Z) - Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。
ラグランジアン分解に基づく新しい手法を提案する。
ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
論文 参考訳(メタデータ) (2020-02-24T17:55:10Z) - Polynomial-Time Exact MAP Inference on Discrete Models with Global
Dependencies [83.05591911173332]
ジャンクションツリーアルゴリズムは、実行時の保証と正確なMAP推論のための最も一般的な解である。
本稿では,ノードのクローン化による新たなグラフ変換手法を提案する。
論文 参考訳(メタデータ) (2019-12-27T13:30:29Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。