Synthesising Recursive Functions for First-Order Model Counting: Challenges, Progress, and Conjectures

First-order model counting (FOMC) is a computational problem that asks to count the models of a sentence in finite- domain first-order logic. Despite being around for more than a decade, practical FOMC algorithms are still unable to compute functions as simple as a factorial. We argue that the capabilities of FOMC algorithms to date are limited by their in- ability to express arbitrary recursive computations. To enable arbitrary recursion, we relax the restrictions that typically ac- company domain recursion and generalise circuits used to ex- press a solution to an FOMC problem to graphs that may contain cycles. To this end, we enhance the most well-established (weighted) FOMC algorithm FORCLIFT with new compilation rules and an algorithm to check whether a recursive call is feasible. These improvements allow the algorithm to construct efficient solutions to counting fundamental structures such as injections and bijections. We end with a few conjectures on what classes of instances could be liftable as a result.