論文の概要: From Width-Based Model Checking to Width-Based Automated Theorem Proving
- arxiv url: http://arxiv.org/abs/2205.10995v3
- Date: Sun, 15 Sep 2024 15:28:05 GMT
- ステータス: 処理完了
- システム内更新日: 2024-09-18 06:00:45.232685
- Title: From Width-Based Model Checking to Width-Based Automated Theorem Proving
- Title（参考訳）: Width-based Model CheckingからWidth-based Automated Theorem Provingへ
- Authors: Mateus de Oliveira Oliveira, Farhad Vadiee,
- Abstract要約: 本稿では,ワイドベースモデルチェックアルゴリズムをグラフ理論の妥当性を検証できるアルゴリズムに変換するための一般的なフレームワークを提案する。
我々のフレームワークはモジュラーであり、木幅や斜め幅を含むグラフのいくつかのよく研究された幅測度に対して適用することができる。
- 参考スコア（独自算出の注目度）: 8.131328180219962
- 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 prove analytically 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$. These upper bounds, which may be regarded as upper-bounds on the size of proofs/disproofs for these conjectures on the class of graphs of treewidth at most $k$, improve significantly on theoretical upper bounds obtained using previously available techniques.
- Abstract（参考訳）: パラメータ化複雑性理論の分野では、グラフ上の組合せ特性に対する幅に基づくモデル検査アルゴリズムの開発とグラフ幅測度の研究が密接に関連している。
本研究では,境界幅のグラフのクラス上でのグラフ理論的予想の妥当性を検証するアルゴリズムに,広い範囲のモデルチェックアルゴリズムを変換する一般的なフレームワークを提案する。
我々のフレームワークはモジュラーであり、木幅や斜め幅を含むグラフのいくつかのよく研究された幅測度に対して適用することができる。
我々のフレームワークの定量的応用として、いくつかの長期グラフ理論予想に対して、入力として$k$の数値を取るアルゴリズムが存在し、$k^{O(1)} において、この予想が木幅のすべてのグラフ上で少なくとも$k$の値で有効であるかどうかを正確に判定するアルゴリズムが存在することを解析的に証明する。
これらの上界は、木幅のグラフのクラスを最大$k$とするこれらの予想の証明や反証のサイズの上界と見なすことができ、既に利用可能な手法を用いて得られる理論上界を著しく改善する。
関連論文リスト
- Differentiable Proximal Graph Matching [40.41380102260085]
微分可能近位グラフマッチング(DPGM)と呼ばれる近位演算子に基づくグラフマッチングアルゴリズムを提案する。
アルゴリズム全体をグラフ親和性行列からノード対応の予測への微分可能な写像とみなすことができる。
数値実験により、PGMは様々なデータセット上で既存のグラフマッチングアルゴリズムより優れていることが示された。
論文 参考訳（メタデータ） (2024-05-26T08:17:13Z) - Encoder Embedding for General Graph and Node Classification [4.178980693837599]
エンコーダの埋め込み行列が大数の法則と中心極限定理を満たすことを証明している。
ある条件下では、クラスごとの正規性を達成し、識別分析による最適な分類を可能にする。
論文 参考訳（メタデータ） (2024-05-24T11:51:08Z) - Homomorphism Counts for Graph Neural Networks: All About That Basis [8.25219440625445]
我々は、よりきめ細かいアプローチを論じ、対象パターンの基底''にすべての構造の準同型数を含む。
これにより計算複雑性の面で追加のオーバーヘッドを発生させずに、より表現力のあるアーキテクチャが得られる。
論文 参考訳（メタデータ） (2024-02-13T16:57:06Z) - Gaussian Entanglement Measure: Applications to Multipartite Entanglement
of Graph States and Bosonic Field Theory [50.24983453990065]
フービニ・スタディ計量に基づく絡み合い尺度は、Cocchiarellaと同僚によって最近導入された。
本稿では,多モードガウス状態に対する幾何絡み合いの一般化であるガウスエンタングルメント尺度(GEM)を提案する。
自由度の高い系に対する計算可能な多部絡み合わせ測度を提供することにより、自由なボゾン場理論の洞察を得るために、我々の定義が利用できることを示す。
論文 参考訳（メタデータ） (2024-01-31T15:50:50Z) - Learning Large-Scale MTP$_2$ Gaussian Graphical Models via Bridge-Block
Decomposition [15.322124183968635]
より小型のサブプロブレムを用いて問題全体を等価に最適化できることを示す。
実践的な側面から、この単純で証明可能な規律は、大きな問題を小さな抽出可能なものに分解するために適用することができる。
論文 参考訳（メタデータ） (2023-09-23T15:30:34Z) - Graph Kernel Neural Networks [53.91024360329517]
本稿では、グラフ上の内部積を計算するカーネル関数であるグラフカーネルを用いて、標準畳み込み演算子をグラフ領域に拡張することを提案する。
これにより、入力グラフの埋め込みを計算する必要のない完全に構造的なモデルを定義することができる。
私たちのアーキテクチャでは,任意の種類のグラフカーネルをプラグインすることが可能です。
論文 参考訳（メタデータ） (2021-12-14T14:48:08Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。