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.
翻译:加权模型计数(WMC)是计算命题公式所有满足赋值(即模型)的加权总和的任务。类似地,加权模型采样(WMS)旨在以与各自权重成比例的概率随机生成模型。WMC和WMS均属于$\#\mathsf{P}$-难复杂度类,难以精确求解。然而,已知若命题公式可被紧凑表示并以一阶逻辑表达,计数问题有时可解。在此类情形下,模型计数问题可在域大小多项式时间内求解,这称为域可提升性。进而产生以下问题:加权模型采样是否同样如此?本文探讨该问题并给出肯定答案。具体而言,本文通过为带计数量词的一阶逻辑两变量片段设计一种在域大小多项式时间内运行的高效采样算法,证明了该片段在采样下的域可提升性。我们进一步表明,即使存在基数约束,该结论依然成立。为实证验证所提方法,我们针对多种用于组合结构均匀生成及统计关系模型采样的不同一阶公式开展实验。结果表明,我们的算法显著优于先进的WMS采样器,从而证实了理论结果。