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 \#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 \textit{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 \textit{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都属于#P-hard复杂度类,难以精确求解。然而,已知若命题公式能以紧凑形式表示并在一阶逻辑中表达,计数问题有时可能易于处理。在此类情况下,模型计数问题可在域大小多项式时间内求解,这被称为**域可提升性**。因此产生以下问题:加权模型采样是否同样如此?本文探讨此问题并给出肯定答案。具体而言,我们通过为带计数量词的一阶逻辑双变量片段设计一个域大小多项式时间的有效采样算法,证明了该片段的**采样域可提升性**。进一步表明,即使在存在基数约束的情况下,该结果仍然成立。为实证验证我们的方法,我们在多种一阶公式上开展实验,这些公式专为组合结构的均匀生成及统计关系模型中的采样而设计。结果表明,我们的算法以显著优势超越当前最先进的WMS采样器,证实了理论结果。