First-order model counting emerged recently as a novel reasoning task, at the core of efficient algorithms for probabilistic logics. We present a Skolemization algorithm for model counting problems that eliminates existential quantifiers from a first-order logic theory without changing its weighted model count. For certain subsets of first-order logic, lifted model counters were shown to run in time polynomial in the number of objects in the domain of discourse, where propositional model counters require exponential time. However, these guarantees apply only to Skolem normal form theories (i.e., no existential quantifiers) as the presence of existential quantifiers reduces lifted model counters to propositional ones. Since textbook Skolemization is not sound for model counting, these restrictions precluded efficient model counting for directed models, such as probabilistic logic programs, which rely on existential quantification. Our Skolemization procedure extends the applicability of first-order model counters to these representations. Moreover, it simplifies the design of lifted model counting algorithms.
On the Approximability of Weighted Model Integration on DNF Structures
University of Oxford（牛津大学）
加权模型计数（Weighted Model Counting，WMC）是计算一个命题公式的所有满足赋值的加权和。WMC是众所周知的是精确求解的#P-困难，但承认一个完全多项式随机逼近方案（FPRAS）时，限制到DNF结构。在这项工作中，我们研究加权模型集成，加权模型计数的推广，其中涉及到真实的变量，除了命题变量，并提出以下问题：是否加权模型集成DNF结构承认FPRAS？基于近似体积计算和近似加权模型计数的经典结果，我们证明了DNF结构上的加权模型积分确实可以近似为一类权重函数。我们的近似算法基于三个子程序，每个子程序都可以是弱（即，近似的），或强的（即，精确）Oracle，并且在所有情况下都有准确性保证。我们通过实验验证了我们的方法在不同大小的随机生成的DNF实例，并表明我们的算法可扩展到大型问题实例，涉及多达1 K个变量，这是目前现有的通用加权模型集成求解器无法达到的。
Solving Combinatorial Counting Problems with Weighted First-Order Model Counting
School of Artificial Intelligence, Jilin University, Changchun, China；State Key Laboratory of Complex \& Critical Software Environment, Beihang University, China；National Research Center for Educational Materials, China；Tengen Intelligence Institute, China；Czech Technical University in Prague, Prague, Czech Republic
Lifted Algorithms for Symmetric Weighted First-Order Model Sampling
Beihang University（北京航空航天大学）；Zhongfa Aviation Institute of Beihang University（北京航空航天大学中法航空学院）；ETH Zurich（苏黎世联邦理工学院）；Czech Technical University in Prague（捷克技术大学布拉格分校）
Towards Projected and Incremental Pseudo-Boolean Model Counting
Grabtaxi Holdings（Grab出租车控股公司）；Grab-NUS AI Lab（Grab-新加坡国立大学人工智能实验室）；Georgia Institute of Technology（佐治亚理工学院）；National University of Singapore（新加坡国立大学）；University of Toronto（多伦多大学）
