論文の概要: From Width-Based Model Checking to Width-Based Automated Theorem Proving
- arxiv url: http://arxiv.org/abs/2205.10995v1
- Date: Mon, 23 May 2022 01:56:52 GMT
- ステータス: 処理完了
- システム内更新日: 2022-05-24 19:52:03.684546
- Title: From Width-Based Model Checking to Width-Based Automated Theorem Proving
- Title(参考訳): 幅ベースモデル検査から幅ベース自動定理証明へ
- Authors: Mateus de Oliveira Oliveira and Farhad Vadiee
- Abstract要約: 本稿では,ワイドベースモデルチェックアルゴリズムをグラフ理論の妥当性を検証できるアルゴリズムに変換するための一般的なフレームワークを提案する。
我々のフレームワークはモジュラーであり、木幅や斜め幅を含むグラフのいくつかのよく研究された幅測度に対して適用することができる。
- 参考スコア(独自算出の注目度): 6.265751530543487
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In the field of parameterized complexity theory, the study of graph width
measures has been intimately connected with the development of width-based
model checking algorithms for combinatorial properties on graphs. In this work,
we introduce a general framework to convert a large class of width-based
model-checking algorithms into algorithms that can be used to test the validity
of graph-theoretic conjectures on classes of graphs of bounded width. Our
framework is modular and can be applied with respect to several well-studied
width measures for graphs, including treewidth and cliquewidth.
As a quantitative application of our framework, we show that for several
long-standing graph-theoretic conjectures, there exists an algorithm that takes
a number $k$ as input and correctly determines in time double-exponential in
$k^{O(1)}$ whether the conjecture is valid on all graphs of treewidth at most
$k$. This improves significantly on upper bounds obtained using previously
available techniques.
- Abstract(参考訳): パラメータ化複雑性理論の分野では、グラフ上の組合せ特性に対する幅に基づくモデル検査アルゴリズムの開発とグラフ幅測度の研究が密接に関連している。
本研究では,境界幅のグラフのクラス上でのグラフ理論的予想の有効性を検証するアルゴリズムに,広い範囲のモデルチェックアルゴリズムを変換する一般的なフレームワークを提案する。
我々のフレームワークはモジュラーであり、treewidth や cliquewidth など、グラフのよく研究された幅測度に関して適用できる。
フレームワークの定量的応用として、長年続くグラフ理論の予想に対して、入力として$k$の数値を取るアルゴリズムが存在し、$k^{O(1)} において、この予想が木幅の全グラフ上で最大$k$で有効であるか否かを正確に決定する。
これにより,従来技術で得られた上限値を大幅に改善する。
関連論文リスト
- Sparse Training of Discrete Diffusion Models for Graph Generation [50.691834214298]
グラフの生成モデルは、各ノードペアの相互作用を予測する必要があるため、スケーラビリティ上の問題に遭遇することが多い。
本稿では,SparseDiffについて紹介する。SparseDiffは,グラフ生成のためのデノナイズ拡散モデルである。
実験結果から, SparseDiffは, 小グラフと大グラフの両方において, 生成性能の同時一致を示す。
論文 参考訳(メタデータ) (2023-11-03T16:50:26Z) - Learning Large-Scale MTP$_2$ Gaussian Graphical Models via Bridge-Block
Decomposition [15.322124183968635]
より小型のサブプロブレムを用いて問題全体を等価に最適化できることを示す。
実践的な側面から、この単純で証明可能な規律は、大きな問題を小さな抽出可能なものに分解するために適用することができる。
論文 参考訳(メタデータ) (2023-09-23T15:30:34Z) - NodeFormer: A Scalable Graph Structure Learning Transformer for Node
Classification [70.51126383984555]
本稿では,任意のノード間のノード信号を効率的に伝搬する全ペアメッセージパッシング方式を提案する。
効率的な計算は、カーナライズされたGumbel-Softmax演算子によって実現される。
グラフ上のノード分類を含む様々なタスクにおいて,本手法の有望な有効性を示す実験を行った。
論文 参考訳(メタデータ) (2023-06-14T09:21:15Z) - Solving Projected Model Counting by Utilizing Treewidth and its Limits [23.81311815698799]
予測モデルカウント(PMC)を解く新しいアルゴリズムを提案する。
いわゆる「ツリー幅」が最も顕著な構造パラメータの1つであるという観測から着想を得て,本アルゴリズムは入力インスタンスの一次グラフの小さなツリー幅を利用する。
論文 参考訳(メタデータ) (2023-05-30T17:02:07Z) - Latent Graph Inference using Product Manifolds [0.0]
遅延グラフ学習のための離散微分可能グラフモジュール(dDGM)を一般化する。
我々の新しいアプローチは、幅広いデータセットでテストされ、元のdDGMモデルよりも優れています。
論文 参考訳(メタデータ) (2022-11-26T22:13:06Z) - Regularization of Mixture Models for Robust Principal Graph Learning [0.0]
D$次元データポイントの分布から主グラフを学習するために,Mixture Modelsの正規化バージョンを提案する。
モデルのパラメータは期待最大化手順によって反復的に推定される。
論文 参考訳(メタデータ) (2021-06-16T18:00:02Z) - Joint Network Topology Inference via Structured Fusion Regularization [70.30364652829164]
結合ネットワークトポロジ推論は、異種グラフ信号から複数のグラフラプラシア行列を学習する標準的な問題を表す。
新規な構造化融合正規化に基づく一般グラフ推定器を提案する。
提案するグラフ推定器は高い計算効率と厳密な理論保証の両方を享受できることを示す。
論文 参考訳(メタデータ) (2021-03-05T04:42:32Z) - Online Dense Subgraph Discovery via Blurred-Graph Feedback [87.9850024070244]
我々は高密度サブグラフ発見のための新しい学習問題を導入する。
まず,確率の高いほぼ最適解を求めるエッジ時間アルゴリズムを提案する。
そして、理論的保証のあるよりスケーラブルなアルゴリズムを設計する。
論文 参考訳(メタデータ) (2020-06-24T11:37:33Z) - Embedding Graph Auto-Encoder for Graph Clustering [90.8576971748142]
グラフ自動エンコーダ(GAE)モデルは、半教師付きグラフ畳み込みネットワーク(GCN)に基づく
我々は、グラフクラスタリングのための特定のGAEベースのモデルを設計し、その理論、すなわち、埋め込みグラフオートエンコーダ(EGAE)と整合する。
EGAEは1つのエンコーダと2つのデコーダで構成される。
論文 参考訳(メタデータ) (2020-02-20T09:53:28Z) - Block-Approximated Exponential Random Graphs [77.4792558024487]
指数乱グラフ(ERG)の分野における重要な課題は、大きなグラフ上の非自明なERGの適合である。
本稿では,非自明なERGに対する近似フレームワークを提案する。
我々の手法は、数百万のノードからなるスパースグラフにスケーラブルである。
論文 参考訳(メタデータ) (2020-02-14T11:42:16Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。