From Width-Based Model Checking to Width-Based Automated Theorem Proving
- URL: http://arxiv.org/abs/2205.10995v1
- Date: Mon, 23 May 2022 01:56:52 GMT
- Title: From Width-Based Model Checking to Width-Based Automated Theorem Proving
- Authors: Mateus de Oliveira Oliveira and Farhad Vadiee
- Abstract summary: 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.
Our framework is modular and can be applied with respect to several well-studied width measures for graphs, including treewidth and cliquewidth.
- Score: 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.
Related papers
- Differentiable Proximal Graph Matching [40.41380102260085]
We introduce an algorithm for graph matching based on the proximal operator, referred to as differentiable proximal graph matching (DPGM)
The whole algorithm can be considered as a differentiable map from the graph affinity matrix to the prediction of node correspondence.
Numerical experiments show that PGM outperforms existing graph matching algorithms on diverse datasets.
arXiv Detail & Related papers (2024-05-26T08:17:13Z) - Encoder Embedding for General Graph and Node Classification [4.178980693837599]
We prove that the encoder embedding matrices satisfies the law of large numbers and the central limit theorem on a per-observation basis.
Under certain condition, it achieves normality on a per-class basis, enabling optimal classification through discriminant analysis.
arXiv Detail & Related papers (2024-05-24T11:51:08Z) - Sparse Training of Discrete Diffusion Models for Graph Generation [45.103518022696996]
We introduce SparseDiff, a novel diffusion model based on the observation that almost all large graphs are sparse.
By selecting a subset of edges, SparseDiff effectively leverages sparse graph representations both during the noising process and within the denoising network.
Our model demonstrates state-of-the-art performance across multiple metrics on both small and large datasets.
arXiv Detail & Related papers (2023-11-03T16:50:26Z) - Learning Large-Scale MTP$_2$ Gaussian Graphical Models via Bridge-Block
Decomposition [15.322124183968635]
We show that the entire problem can be equivalently optimized through several smaller-scaled sub-problems.
From practical aspect, this simple and provable discipline can be applied to break down a large problem into small tractable ones.
arXiv Detail & Related papers (2023-09-23T15:30:34Z) - NodeFormer: A Scalable Graph Structure Learning Transformer for Node
Classification [70.51126383984555]
We introduce a novel all-pair message passing scheme for efficiently propagating node signals between arbitrary nodes.
The efficient computation is enabled by a kernerlized Gumbel-Softmax operator.
Experiments demonstrate the promising efficacy of the method in various tasks including node classification on graphs.
arXiv Detail & Related papers (2023-06-14T09:21:15Z) - Solving Projected Model Counting by Utilizing Treewidth and its Limits [23.81311815698799]
We introduce a novel algorithm to solve projected model counting (PMC)
Inspired by the observation that the so-called "treewidth" is one of the most prominent structural parameters, our algorithm utilizes small treewidth of the primal graph of the input instance.
arXiv Detail & Related papers (2023-05-30T17:02:07Z) - Graph Kernel Neural Networks [53.91024360329517]
We propose to use graph kernels, i.e. kernel functions that compute an inner product on graphs, to extend the standard convolution operator to the graph domain.
This allows us to define an entirely structural model that does not require computing the embedding of the input graph.
Our architecture allows to plug-in any type of graph kernels and has the added benefit of providing some interpretability.
arXiv Detail & Related papers (2021-12-14T14:48:08Z) - Joint Network Topology Inference via Structured Fusion Regularization [70.30364652829164]
Joint network topology inference represents a canonical problem of learning multiple graph Laplacian matrices from heterogeneous graph signals.
We propose a general graph estimator based on a novel structured fusion regularization.
We show that the proposed graph estimator enjoys both high computational efficiency and rigorous theoretical guarantee.
arXiv Detail & Related papers (2021-03-05T04:42:32Z) - Online Dense Subgraph Discovery via Blurred-Graph Feedback [87.9850024070244]
We introduce a novel learning problem for dense subgraph discovery.
We first propose a edge-time algorithm that obtains a nearly-optimal solution with high probability.
We then design a more scalable algorithm with a theoretical guarantee.
arXiv Detail & Related papers (2020-06-24T11:37:33Z) - Embedding Graph Auto-Encoder for Graph Clustering [90.8576971748142]
Graph auto-encoder (GAE) models are based on semi-supervised graph convolution networks (GCN)
We design a specific GAE-based model for graph clustering to be consistent with the theory, namely Embedding Graph Auto-Encoder (EGAE)
EGAE consists of one encoder and dual decoders.
arXiv Detail & Related papers (2020-02-20T09:53:28Z) - Block-Approximated Exponential Random Graphs [77.4792558024487]
An important challenge in the field of exponential random graphs (ERGs) is the fitting of non-trivial ERGs on large graphs.
We propose an approximative framework to such non-trivial ERGs that result in dyadic independence (i.e., edge independent) distributions.
Our methods are scalable to sparse graphs consisting of millions of nodes.
arXiv Detail & Related papers (2020-02-14T11:42:16Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.