First-Order Model Counting and Sampling

Why are some combinatorial structures easy to count and sample, while others are not? For example, the number of permutations is given by a simple factorial, and there are efficient textbook algorithms to generate permutations uniformly at random. But what if we ask instead: how many graphs on n vertices satisfy a given property or what if we want the permutations to satisfy some additional constraints? Is there a systematic way to identify which such counting and sampling problems are tractable? First-order model counting (FOMC) and its sampling variant (FOMS) provide a unifying framework for addressing a non-trivial subset of these questions.

In FOMC, we ask how many structures over a finite domain satisfy a given first-order sentence, and FOMS extends this to sampling such structures. Following the seminal results of Van den Broeck (2011) and Van den Broeck, Meert, and Darwiche (2014), which showed that the two-variable fragment is tractable for FOMC, larger polynomial-time solvable classes have been identified in the past decade and extended to FOMS. In this talk, we will survey these developments and illustrate applications: automating routine counting in combinatorics and probability (such as the classic Secret Santa problem, which asks in how many ways n people can exchange gifts so that nobody receives their own), building a database of “interesting” combinatorial integer sequences, and providing new insights into classical problems in algorithmic game theory.