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

TL;DR

The paper addresses the hardness of conditioning WFOMC on binary evidence by restricting the evidence to yield a Gaifman graph of bounded treewidth. It develops a dynamic-programming algorithm for the UFO^2 fragment (extensible to FO^2 and C^2 with cardinality constraints) that runs in polynomial time in the domain size, leveraging nice tree decompositions and a recursion over 1-types and 2-tables. The approach enables tractable counting in combinatorial problems, exemplified by a polynomial-time solution to the stable seating arrangement problem on bounded-treewidth graphs with bounded degree, and is supported by experiments showing scalability against existing model counters. The work thus extends domain-liftability to a broader class of WFOMC problems with binary evidence and demonstrates practical applicability through MLN-based problem encodings. Overall, it advances lifted inference by preserving symmetry and tractability in a class of binary-evidence WFOMC problems with meaningful real-world applications.

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.

Figures (4)

• Figure 1: An example of the Gaifman graph (left) of closed-world binary evidence and its nice tree decomposition (right). The leaf, introduce, forget and join nodes are colored in white, blue, green and orange respectively. The last forget nodes are omitted for simplicity.
• Figure 2: Time to compute the model count of friends and smokers problem with binary evidence
• Figure 3: Time to compute the model count of friends and smokers problem with binary evidence, fixing $|\Delta| = 60$ for varying size of friend cliques.
• Figure 4: Inference times on Watts-Strogatz model, $K = 2$ and the simplified model, $K = 2$ and $M = \lfloor \frac{|\Delta| + 1}{2} \rfloor$. We use full line for a ring lattice starting graph and dashed line for cliques starting graph.

Theorems & Definitions (20)

• Remark 1.1
• Example 2.1
• Definition 2.1: Weighted First Order Model Counting
• Example 2.2
• Definition 2.2: 1-Type
• Definition 2.3: 2-Table
• Definition 2.4: 1-Type Configuration
• Definition 2.5: Open-World Evidence
• Definition 2.6: Closed-World Evidence
• Remark 2.1