First-order model counting (FOMC) is a computational problem that asks to count the models of a sentence in finite-domain first-order logic. In this paper, we argue that the capabilities of FOMC algorithms to date are limited by their inability to express many types of recursive computations. To enable such computations, we relax the restrictions that typically accompany domain recursion and generalise the circuits used to express a solution to an FOMC problem to directed graphs that may contain cycles. To this end, we adapt the most well-established (weighted) FOMC algorithm ForcLift to work with such graphs and introduce new compilation rules that can create cycle-inducing edges that encode recursive function calls. These improvements allow the algorithm to find efficient solutions to counting problems that were previously beyond its reach, including those that cannot be solved efficiently by any other exact FOMC algorithm. We end with a few conjectures on what classes of instances could be domain-liftable as a result.

翻译：一阶模型计数（FOMC）是一个计算问题，要求计算有限域一阶逻辑中某个句子的模型数量。本文指出，迄今为止FOMC算法的能力受限于其无法表达多种类型的递归计算。为了实现此类计算，我们放宽了通常伴随域递归的限制，并将用于表达FOMC问题解的电路泛化为可能包含环的有向图。为此，我们调整了最成熟的（加权）FOMC算法ForcLift以适应此类图，并引入了新的编译规则，这些规则能够生成编码递归函数调用的环路诱导边。这些改进使得算法能够求解此前无法触及的计数问题，包括其他精确FOMC算法无法高效求解的问题。最后，我们提出若干猜想，探讨哪些实例类别可因此成为域可提升的。