Tractable Weighted First-Order Model Counting with Bounded Treewidth Binary Evidence

• URL: http://arxiv.org/abs/2511.09174v1
• Date: Thu, 13 Nov 2025 01:37:37 GMT
• Title: Tractable Weighted First-Order Model Counting with Bounded Treewidth Binary Evidence
• Authors: Václav Kůla, Qipeng Kuang, Yuyi Wang, Yuanhong Wang, Ondřej Kuželka,
• Abstract summary: The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a domain.<n>We present an algorithm for computing WFOMC for the two-tree fragments $textFO2$ and $text2$ conditioned by such binary evidence.
• Score: 2.5551288018371157
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. Conditioning WFOMC on evidence -- fixing the truth values of a set of ground literals -- has been shown impossible in time polynomial in the domain size (unless $\mathsf{\#P \subseteq FP}$) even for fragments of logic that are otherwise tractable for WFOMC without evidence. In this work, we address the barrier by restricting the binary evidence to the case where the underlying Gaifman graph has bounded treewidth. We present a polynomial-time algorithm in the domain size for computing WFOMC for the two-variable fragments $\text{FO}^2$ and $\text{C}^2$ conditioned on such binary evidence. Furthermore, we show the applicability of our algorithm in combinatorial problems by solving the stable seating arrangement problem on bounded-treewidth graphs of bounded degree, which was an open problem. We also conducted experiments to show the scalability of our algorithm compared to the existing model counting solvers.

Related papers

• Learning Intersections of Two Margin Halfspaces under Factorizable Distributions [56.51474048985742]
  Learning intersections of halfspaces is a central problem in Computational Learning Theory.<n>Even for just two halfspaces, it remains a major open question whether learning is possible in time.<n>We introduce a novel algorithm that provably circumvents the CSQ hardness barrier.
  arXiv  Detail & Related papers  (2025-11-13T00:28:24Z)
• Maximum a Posteriori Inference for Factor Graphs via Benders' Decomposition [0.38233569758620056]
  We present a method for maximum a-posteriori inference in general Bayesian factor models. We derive MAP estimation algorithms for the Bayesian Gaussian mixture model and latent Dirichlet allocation.
  arXiv  Detail & Related papers  (2024-10-24T19:57:56Z)
• Lifted Algorithms for Symmetric Weighted First-Order Model Sampling [7.007419073974192]
  We prove the domain-liftability under sampling for the two-variables fragment of first-order logic with counting quantifiers. We then show that this result continues to hold even in the presence of cardinality constraints. Our algorithm outperforms a start-of-the-art WMS sampler by a substantial margin.
  arXiv  Detail & Related papers  (2023-08-17T07:40:47Z)
• Efficient Computation of Counterfactual Bounds [44.4263314637532]
  We compute exact counterfactual bounds via algorithms for credal nets on a subclass of structural causal models. We evaluate their accuracy by providing credible intervals on the quality of the approximation.
  arXiv  Detail & Related papers  (2023-07-17T07:59:47Z)
• 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)
• Robust affine point matching via quadratic assignment on Grassmannians [50.366876079978056]
  Robust Affine Matching with Grassmannians (RoAM) is a new algorithm to perform affine registration of point clouds. The algorithm is based on minimizing the Frobenius distance between two elements of the Grassmannian.
  arXiv  Detail & Related papers  (2023-03-05T15:27:24Z)
• Weighted First Order Model Counting with Directed Acyclic Graph Axioms [7.766921168069532]
  Probabilistic inference and learning in many SRL can be reduced to Weighted First Model Counting (WFOMC) WFOMC is known to be intractable ($mathrm#P$ complete) We show that the fragment $mathrmC2$ with a Directed Acyclic Graph (DAG)exclusion, i.e., a axiomatized to represent axiom DAG, is domain liftable.
  arXiv  Detail & Related papers  (2023-02-20T08:35:13Z)
• Diffusion models as plug-and-play priors [98.16404662526101]
  We consider the problem of inferring high-dimensional data $mathbfx$ in a model that consists of a prior $p(mathbfx)$ and an auxiliary constraint $c(mathbfx,mathbfy)$. The structure of diffusion models allows us to perform approximate inference by iterating differentiation through the fixed denoising network enriched with different amounts of noise.
  arXiv  Detail & Related papers  (2022-06-17T21:11:36Z)
• Partial Counterfactual Identification from Observational and Experimental Data [83.798237968683]
  We develop effective Monte Carlo algorithms to approximate the optimal bounds from an arbitrary combination of observational and experimental data. Our algorithms are validated extensively on synthetic and real-world datasets.
  arXiv  Detail & Related papers  (2021-10-12T02:21:30Z)
• Weighted Model Counting in the two variable fragment with Cardinality Constraints: A Closed Form Formula [7.766921168069532]
  Weighted First-Order Model Counting (WFOMC) computes the weighted sum of the models of a first-order theory on a given finite domain. We introduce the concept of lifted interpretations as a tool for formulating inferences for WFOMC. We then expand this closed-form to incorporate existential quantifiers and cardinality constraints without losing domain-liftability.
  arXiv  Detail & Related papers  (2020-09-25T13:50:18Z)
• An Integer Linear Programming Framework for Mining Constraints from Data [81.60135973848125]
  We present a general framework for mining constraints from data. In particular, we consider the inference in structured output prediction as an integer linear programming (ILP) problem. We show that our approach can learn to solve 9x9 Sudoku puzzles and minimal spanning tree problems from examples without providing the underlying rules.
  arXiv  Detail & Related papers  (2020-06-18T20:09:53Z)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  A fundamental component of neural network verification is the computation of bounds on the values their outputs can take. We propose a novel approach based on Lagrangian Decomposition. We show that we obtain bounds comparable with off-the-shelf solvers in a fraction of their running time.
  arXiv  Detail & Related papers  (2020-02-24T17:55:10Z)
• Polynomial-Time Exact MAP Inference on Discrete Models with Global Dependencies [83.05591911173332]
  junction tree algorithm is the most general solution for exact MAP inference with run-time guarantees. We propose a new graph transformation technique via node cloning which ensures a run-time for solving our target problem independently of the form of a corresponding clique tree.
  arXiv  Detail & Related papers  (2019-12-27T13:30:29Z)

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.