Synthesising Recursive Functions for First-Order Model Counting
21/4/2023
Speaker
Abstract
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 talk, I am going to 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.
Bio
Paulius Dilkas is a Research Fellow at the PLSE lab, NUS, hosted by Kuldeep Meel. His research is on model counting algorithms for propositional and first-order logic, with a focus on practical efficiency and applications to probabilistic inference. Paulius recently finished his PhD at the University of Edinburgh, UK, supervised by Vaishak Belle and titled 'Generalising Weighted Model Counting'.