arXiv subjects

Václav Kůla

Publications and source records attributed to Václav Kůla.

3 recordsLinked to original sources

arXiv2026

Weighted First-Order Model Counting over Ordered Domains

The Weighted First-Order Model Counting Problem (WFOMC) asks for the weighted sum of models of a first-order logical sentence over a domain. It is a fundamental problem in statistical relational learning, with applications extending to enumerative combinatorics and graph polynomials. Computing WFOMC for the three-variable fragment is $\mathsf{\#P}_1$-hard, whereas polynomial-time algorithms exist for the two-variable fragment and its extensions by cardinality constraints and counting quantifiers. In this work, we explore computing WFOMC in polynomial time over linearly ordered domains, enabling tractable reasoning across inference scenarios and combinatorial problems involving sequences. Because encoding a linear order in standard first-order logic requires three variables, negating our polynomial-time aspirations, we add a linear order axiom directly to the language. This forces one predicate to impose a total ordering on domain elements. We first prove that WFOMC with the linear order axiom can be solved in time polynomial in the domain size. We then extend this result to ordered domains with access to successor relations. While this holds when successors are explicitly defined via the linear order, we demonstrate an alternative implicit approach where successor relations are part of the axiom. This implicit method exhibits significantly better performance on all tested instances, sometimes providing exponential runtime improvements. Finally, we analyze scenarios with two distinct linear orders. We show that WFOMC over the two-variable fragment with two linear orders is $\mathsf{\#P}_1$-hard. However, we develop a polynomial-time algorithm for WFOMC with one linear order and a successor relation of another, pushing the intractability barrier further, yet still leaving the question of how close to a second full linear order one can get.

cs.LO↗

arXiv2025

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

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.

cs.LO↗

arXiv2025

Weighted First Order Model Counting for Two-variable Logic with Axioms on Two Relations

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. The boundary between fragments for which WFOMC can be computed in polynomial time relative to the domain size lies between the two-variable fragment ($\text{FO}^2$) and the three-variable fragment ($\text{FO}^3$). It is known that WFOMC for \FOthree{} is $\mathsf{\#P_1}$-hard while polynomial-time algorithms exist for computing WFOMC for $\text{FO}^2$ and $\text{C}^2$, possibly extended by certain axioms such as the linear order axiom, the acyclicity axiom, and the connectedness axiom. All existing research has concentrated on extending the fragment with axioms on a single distinguished relation, leaving a gap in understanding the complexity boundary of axioms on multiple relations. In this study, we explore the extension of the two-variable fragment by axioms on two relations, presenting both negative and positive results. We show that WFOMC for $\text{FO}^2$ with two linear order relations and $\text{FO}^2$ with two acyclic relations are $\mathsf{\#P_1}$-hard. Conversely, we provide an algorithm in time polynomial in the domain size for WFOMC of $\text{C}^2$ with a linear order relation, its successor relation and another successor relation.

cs.LO↗