Lifted Algorithms for Symmetric Weighted First-Order Model Sampling

TL;DR

This work develops a theory and practical algorithms for weighted first-order model sampling (WFOMS), proving domain-liftability for the two-variable fragments UFO^2, FO^2, and C^2 (including counting quantifiers) and extending liftability to cases with cardinality constraints. The core method combines a two-phase sampler (sampling 1-types then 2-tables) with domain recursion and Tseitin-based encodings to handle existential constraints, enabling polynomial-time sampling in the domain size. The paper provides normal-form transformations, sound reductions, and a detailed complexity analysis, complemented by extensive experiments on combinatorial-structure generation and Markov logic networks that demonstrate substantial performance gains over prior samplers. These results establish WFOMS as a viable and scalable paradigm for sampling in statistical-relational settings and pave the way for broader extensions to richer logics and more complex constraints.

Abstract

Weighted model counting (WMC) is the task of computing the weighted sum of all satisfying assignments (i.e., models) of a propositional formula. Similarly, weighted model sampling (WMS) aims to randomly generate models with probability proportional to their respective weights. Both WMC and WMS are hard to solve exactly, falling under the $\#\mathsf{P}$-hard complexity class. However, it is known that the counting problem may sometimes be tractable, if the propositional formula can be compactly represented and expressed in first-order logic. In such cases, model counting problems can be solved in time polynomial in the domain size, and are known as domain-liftable. The following question then arises: Is it also the case for weighted model sampling? This paper addresses this question and answers it affirmatively. Specifically, we prove the domain-liftability under sampling for the two-variables fragment of first-order logic with counting quantifiers in this paper, by devising an efficient sampling algorithm for this fragment that runs in time polynomial in the domain size. We then further show that this result continues to hold even in the presence of cardinality constraints. To empirically verify our approach, we conduct experiments over various first-order formulas designed for the uniform generation of combinatorial structures and sampling in statistical-relational models. The results demonstrate that our algorithm outperforms a start-of-the-art WMS sampler by a substantial margin, confirming the theoretical results.

Figures (6)

• Figure 1: A sampling step for an undirected graph with no isolated vertices: (a) begins with an initial graph that has no edges, and in the more general sampling problem, $V_\forall = V_\exists = \{v_1,v_2,v_3,v_4\}$; (b) sample edges for the vertex $v_1$; (c) remove the vertex $v_1$ with its sampled edges; (d) and obtain a graph with some vertices already non-isolated ($v_2$ and $v_3$), resulting in a new sampling problem with $V_\forall' = \{v_2,v_3,v_4\}$ and $V_\exists' = \{v_4\}$.
• Figure 2: An example of sampling a substructure. There are two cell types, denoted by and , and two 2-tables, denoted by and . The sampled substructure $\mathcal{A}_t$ is represented on the left, whose 2-tables configuration is $(g_{\text{\faCircle{}}, \text{{}}}^{\mathcal{A}_t}, g_{\text{\faCircle{}}, \text{{}}}^{\mathcal{A}_t}, g_{\text{\faCircleThin{}}, \text{{}}}^{\mathcal{A}_t}, g_{\text{\faCircleThin{}}, \text{{}}}^{\mathcal{A}_t}) = (1, 2, 2, 1)$. With the relaxations of cell types defined above the arrow, where, e.g., $\text{\faCircle{}}=\text{\faCircleThin{}}$ means the relaxed cell type of under is , the reduced cell types for each element is presented on the right. One can easily obtain the reduced cell configuration from the 2-table configuration $(g_{\text{\faCircle{}}, \text{{}}}^{\mathcal{A}_t}, g_{\text{\faCircle{}}, \text{{}}}^{\mathcal{A}_t}, g_{\text{\faCircleThin{}}, \text{{}}}^{\mathcal{A}_t}, g_{\text{\faCircleThin{}}, \text{{}}}^{\mathcal{A}_t})$.
• Figure 3: An illustration of domain recursion for the WFOMS problem in Example \ref{['ex:2regular_colored']}. The vertices $v_1$ and $v_4$ are colored red, while the vertices $v_2$ and $v_3$ are not colored, according to the sampled 1-types. The number shown in each vertex corresponds to its block type, denoting the number of neighbors that the vertex should or should not have, e.g., $v_1$ should have exactly two neighbors, while $v_2$ should not have two neighbors. In each domain recursion step, the block types of the selected element are relaxed according to the sampled edges. Note that in the final step, the edge between $v_1$ and $v_4$ is always sampled, as the block type of $v_1$ and $v_3$ requires them to have at least one neighbor.
• Figure 4: Uniformity comparison between an ideal sampler (IS) and our weighted model sampler.
• Figure 5: Conformity testing for the count distribution of MLNs.

Theorems & Definitions (44)

• Definition 1: Weight of literals
• Definition 2: Weighted first-order model counting
• Proposition 1
• Example 1
• Definition 3: Configuration space
• Definition 4: Weighted first-order model sampling
• Example 2
• Definition 5: Sound reduction
• Theorem 1
• Example 3