A Fast Model Counting Algorithm for Two-Variable Logic with Counting and Modulo Counting Quantifiers

• URL: http://arxiv.org/abs/2605.03391v1
• Date: Tue, 05 May 2026 05:58:39 GMT
• Title: A Fast Model Counting Algorithm for Two-Variable Logic with Counting and Modulo Counting Quantifiers
• Abstract summary: We introduce IncrementalWFOMC3, a lifted algorithm for WFOMC on $mathbfC2$ and its modulo counting extension, $mathbf2_textmod$.<n>First, we derive a tighter data-complexity bound for WFOMC in $mathbfC2$, reducing the degree from quadratic to linear runtime in the counting parameters.<n>Second, we prove that $mathbfC2mod$ is domain-liftable, extending tractability from $mathbfC2$ to a richer with native mod
• Score: 14.737223920007722
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Weighted first-order model counting (WFOMC) is a central task in lifted probabilistic inference: It asks for the weighted sum of all models of a first-order sentence over a finite domain. A long line of work has identified domain-liftable fragments of first-order logic, that is, syntactic classes for which WFOMC can be solved in time polynomial in the domain size. Among them, the two-variable fragment with counting quantifiers, $\mathbf{C}^2$, is one of the most expressive known liftable fragments. Existing algorithms for $\mathbf{C}^2$, however, establish tractability through multi-stage reductions that eliminate counting quantifiers via cardinality constraints, which introduces substantial practical overhead as the domain size grows. In this paper, we introduce IncrementalWFOMC3, a lifted algorithm for WFOMC on $\mathbf{C}^2$ and its modulo counting extension, $\mathbf{C}^2_{\text{mod}}$. Instead of relying on reduction techniques, IncrementalWFOMC3 operates directly on a Scott normal form that retains counting quantifiers throughout inference. This direct treatment yields two main results. First, we derive a tighter data-complexity bound for WFOMC in $\mathbf{C}^2$, reducing the degree of the polynomial from quadratic to linear in the counting parameters. Second, we prove that $\mathbf{C}^2_{\text{mod}}$ is domain-liftable, extending tractability from $\mathbf{C}^2$ to a richer fragment with native modulo counting support. Finally, our empirical evaluation shows that IncrementalWFOMC3 delivers orders-of-magnitude runtime improvements and better scalability than both existing WFOMC algorithms and state-of-the-art propositional model counters.

Related papers

• A Sharp Barrier for Consistent Submodular Maximization: Any Improvement over $2-\sqrt{2}$ Entails Exponential Queries or Linear Recourse [50.69285844345291]
  We study tradeoff between solution quality and stability when elements arrive over time.<n>Our algorithm has a future implementation for rational oracle$ with $O(varepsilon-1)$ recourse and separate the existence of universal-price certificates from their efficient algorithms.
  arXiv  Detail & Related papers  (2026-09-09T10:13:43Z)
• Tractable Weighted First-Order Model Counting with Bounded Treewidth Binary Evidence [2.5551288018371157]
  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.
  arXiv  Detail & Related papers  (2025-11-12T10:12:39Z)
• Effective Policy Learning for Multi-Agent Online Coordination Beyond Submodular Objectives [64.16056378603875]
  We present two policy learning algorithms for multi-agent online coordination problem.<n>The first one, textttMA-SPL, can achieve the optimal $(fracce)$-approximation for the MA-OC problem.<n>The second online algorithm named textttMA-MPL can simultaneously maintain the same approximation ratio.
  arXiv  Detail & Related papers  (2025-09-26T17:16:34Z)
• Weighted First Order Model Counting for Two-variable Logic with Axioms on Two Relations [5.843053614714943]
  We show that WFOMC for $textFO2$ with two linear order relations and $textFO2$ with two acyclic relations are $mathsf#P_1$-hard.<n>We provide an algorithm in time in the domain size for WFOMC of $textC2$ with a linear order relation, its successor relation and another successor relation.
  arXiv  Detail & Related papers  (2025-08-15T14:54:17Z)
• Lifted Inference beyond First-Order Logic [8.577974472273256]
  We show that any $mathrmC2$ sentence remains domain liftable when one of its relational properties is a directed acyclic graph, a connected graph, a tree or a forest.<n>Our results rely on a novel and general methodology of "counting by splitting"
  arXiv  Detail & Related papers  (2023-08-22T18:58:21Z)
• 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)
• Refined Regret for Adversarial MDPs with Linear Function Approximation [50.00022394876222]
  We consider learning in an adversarial Decision Process (MDP) where the loss functions can change arbitrarily over $K$ episodes. This paper provides two algorithms that improve the regret to $tildemathcal O(K2/3)$ in the same setting.
  arXiv  Detail & Related papers  (2023-01-30T14:37:21Z)
• Average-Case Complexity of Tensor Decomposition for Low-Degree Polynomials [93.59919600451487]
  "Statistical-computational gaps" occur in many statistical inference tasks. We consider a model for random order-3 decomposition where one component is slightly larger in norm than the rest. We show that tensor entries can accurately estimate the largest component when $ll n3/2$ but fail to do so when $rgg n3/2$.
  arXiv  Detail & Related papers  (2022-11-10T00:40:37Z)
• Lifted Inference with Linear Order Axiom [0.0]
  We consider the task of weighted first-order model counting (WFOMC) We show that WFOMC of any logical sentence with at most two logical variables can be done in time in $n$. We present a new dynamic programming-based algorithm which can compute WFOMC with linear order in time in $n$.
  arXiv  Detail & Related papers  (2022-11-02T14:38:01Z)
• TURF: A Two-factor, Universal, Robust, Fast Distribution Learning Algorithm [64.13217062232874]
  One of its most powerful and successful modalities approximates every distribution to an $ell$ distance essentially at most a constant times larger than its closest $t$-piece degree-$d_$. We provide a method that estimates this number near-optimally, hence helps approach the best possible approximation.
  arXiv  Detail & Related papers  (2022-02-15T03:49:28Z)
• Higher-order Derivatives of Weighted Finite-state Machines [68.43084108204741]
  This work examines the computation of higher-order derivatives with respect to the normalization constant for weighted finite-state machines. We provide a general algorithm for evaluating derivatives of all orders, which has not been previously described in the literature. Our algorithm is significantly faster than prior algorithms.
  arXiv  Detail & Related papers  (2021-06-01T19:51:55Z)
• Revisiting Modified Greedy Algorithm for Monotone Submodular Maximization with a Knapsack Constraint [75.85952446237599]
  We show that a modified greedy algorithm can achieve an approximation factor of $0.305$. We derive a data-dependent upper bound on the optimum. It can also be used to significantly improve the efficiency of such algorithms as branch and bound.
  arXiv  Detail & Related papers  (2020-08-12T15:40:21Z)

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.