Lifted Algorithms for Symmetric Weighted First-Order Model Sampling

TL;DR

This paper proves that weighted model sampling is domain-liftable for the two-variable fragment of first-order logic with counting quantifiers, providing an efficient polynomial-time sampling algorithm and demonstrating its practical superiority over existing methods.

Contribution

It introduces the first domain-liftable sampling algorithm for the two-variable fragment of first-order logic with counting quantifiers, extending liftability to sampling tasks.

Findings

The algorithm runs in polynomial time in the domain size.

It outperforms state-of-the-art WMS samplers in experiments.

The approach remains effective even with added cardinality 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.