From Width-Based Model Checking to Width-Based Automated Theorem Proving

• URL: http://arxiv.org/abs/2205.10995v3
• Date: Sun, 15 Sep 2024 15:28:05 GMT
• Title: From Width-Based Model Checking to Width-Based Automated Theorem Proving
• Authors: Mateus de Oliveira Oliveira, 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: 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.

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)
• Homomorphism Counts for Graph Neural Networks: All About That Basis [8.25219440625445]
  We argue for a more fine-grained approach, which incorporates the homomorphism counts of all structures in the basis'' of the target pattern. This yields strictly more expressive architectures without incurring any additional overhead in terms of computational complexity.
  arXiv  Detail & Related papers  (2024-02-13T16:57:06Z)
• Gaussian Entanglement Measure: Applications to Multipartite Entanglement of Graph States and Bosonic Field Theory [50.24983453990065]
  An entanglement measure based on the Fubini-Study metric has been recently introduced by Cocchiarella and co-workers. We present the Gaussian Entanglement Measure (GEM), a generalization of geometric entanglement measure for multimode Gaussian states. By providing a computable multipartite entanglement measure for systems with a large number of degrees of freedom, we show that our definition can be used to obtain insights into a free bosonic field theory.
  arXiv  Detail & Related papers  (2024-01-31T15:50:50Z)
• 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)
• 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.