Model Counting and Sampling in First-Order Logic Ondřej Kuželka1 1 Faculty of Electrical Engineering, Czech Technical University in Prague, Czech Republic Abstract First-order model counting (FOMC) asks to count models of a first-order logic sentence over a given set of domain elements. Its weighted variant, WFOMC, generalizes FOMC by assigning weights to the models and has applications among others in statistical relational learning. Several non-trivial classes of WFOMC problems that can be solved in time polynomial in the number of domain elements were identified in the literature over the past decade, since the two seminal paper by Van den Broeck (2011) and Van den Broeck, Meert and Darwiche (2014) established tractability of FO2 for WFOMC. This talk is about recent developments on WFOMC and the related problem of weighted first-order model sampling (WFOMS). We also discuss applications of WFOMC and WFOMS, such as automated solving of problems from enumerative combinatorics and elementary probability theory. Keywords Model counting, sampling, first-order Logic, 1. Weighted First-Order Model Counting Weighted first-order model counting (WFOMC) is the task of computing the weighted sum of models of a given first-order logic sentence [1]. It has applications in statistical relational learning [2] and it is also relevant for probability theory and combinatorics [3, 4]. Formally, given a set of domain elements ∆ and two functions 𝑤(𝑃 ) and 𝑤(𝑃 ) mapping predicate symbols to real numbers, we define WFOMC as ∑︁ WFOMC(Ψ, ∆, 𝑤, 𝑤) = 𝑊 (𝜔, 𝑤, 𝑤), 𝜔:𝜔|=Ψ where 𝑊 (𝜔), i.e. the weight of 𝜔, is computed as ∏︁ ∏︁ 𝑊 (𝜔, 𝑤, 𝑤) = 𝑤(pred(𝑙)) 𝑤(pred(𝑙)). 𝜔|=𝑙 𝜔|=¬𝑙 Example 1 (Illustrating the notion of WFOMC). Let us have a domain ∆ = {𝐴, 𝐵}, and suppose that we only have two predicates heads and tails, with weights given as 𝑤(heads) = 2, 𝑤(tails) = 𝑤(heads) = 𝑤(tails) = 1. We will want to compute the WFOMC of the sentence Γ = ∀𝑥 : (heads(𝑥)∨tails(𝑥))∧(¬heads(𝑥)∨¬tails(𝑥)). There are four models of Γ on the domain DL 2024: 37th International Workshop on Description Logics, June 18–21, 2024, Bergen, Norway $ ondrej.kuzelka@fel.cvut.cz (O. Kuželka) € https://ida.fel.cvut.cz/~kuzelka/ (O. Kuželka)  0000-0002-0877-7063 (O. Kuželka) © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings ∆: 𝜔1 = {heads(𝐴), heads(𝐵)}, 𝜔2 = {heads(𝐴), tails(𝐵)}, 𝜔3 = {tails(𝐴), heads(𝐴)} and 𝜔4 = {tails(𝐴), tails(𝐵)}. The resulting first-order model count is FOMC(Γ, ∆) = 4 and the weighted model count is WFOMC(Γ, 𝑤, 𝑤, ∆) = 4 + 2 + 2 + 1 = 9. Example 2. Consider the following variant of the Secret Santa game. There are 𝑛 people attending the Christmas party. Each person is supposed to give presents to 𝑘 other people and receive 𝑘 presents.1 The organizer decides to let everyone draw names from 𝑘 hats each of which contains everyone’s name once. The participants then come and each of them draws one name at random from each hat. We ask what is the probability that no one, at the same time, (i) draws their own name and (ii) draws the same name more than once. When 𝑘 = 1, the solution is known since the 18th century and it is the ratio of the number of derangements (i.e., permutations without fixed points) and the number of permutations on 𝑛 elements. For 𝑘 > 1 the problem could still be solved by hand, but with non-trivial effort and with good knowledge of combinatorics. The same problem could, however, also be solved automatically using WFOMC in polynomial time because it can be encoded in the two-variable fragment of first-order logic with counting quantifiers C2 [5], which is known to be tractable [6] (what we mean by “tractable” is explained in Section 3). The C2 sentence with which we can achieve it is: 𝑘 ⋀︁ ∀𝑥∃=1 𝑦 Draw𝑖 (𝑥, 𝑦) ∧ ∀𝑦∃=1 𝑥 Draw𝑖 (𝑥, 𝑦) ∧ ∀𝑥 ¬Draw𝑖 (𝑥, 𝑥) ∧ (︀ )︀ Ψ= 𝑖=1 𝑘 ⋀︁ ⋀︁ (∀𝑥∀𝑦 ¬Draw𝑖 (𝑥, 𝑦) ∨ ¬Draw𝑗 (𝑥, 𝑦)) . 𝑖=1 𝑗<𝑖 Here, Draw𝑖 (𝑥, 𝑦) represents that 𝑥 drew the name 𝑦 from the hat 𝑖. To compute the desired probability, we just need to divide the WFOMC of the sentence Ψ on a domain of size 𝑛 by (𝑛!)𝑘 which is the total number of all possible draws (obviously, if we did not know factorials, we could compute this number by WFOMC as well). 2. Weighted First-Order Model Sampling Another useful task one might need to solve is, given a first-order logic sentence, a domain and weighting functions, to sample a model of the sentence with probability proportional to its weight. This problem is known as weighted first-order model sampling (WFOMS) [7]. It has again applications in statistical relational learning, as it allows sampling from Markov logic networks [8, 9, 10], but its potential applications are much broader—it generally provides a principled approach for efficient sampling of combinatorial structures. Example 3. Suppose that after computing the probability of a successful draw in the Secret Santa game from Example 2 (a successful draw is one in which no one got their own name and no one got name of anyone else more than once), we conclude that the probability is too low for this procedure to be practical. Then we might want to sample an assignment of who should give presents to whom automatically. To achieve that we can sample models of the C2 sentence from Example 2 using WFOMS. It turns out that sampling is also tractable for sentences from the C2 fragment [10]. 1 In the normal variant of the Secret Santa game, 𝑘 = 1. 3. Tractability An important question about WFOMC and WFOMS is: How hard are they? First, it is not difficult to observe that there is no hope for a WFOMC algorithm that would scale polynomially with the size of the first-order logic sentence even if the sentence was guaranteed to have just one logical variable (unless P = #P). Therefore focus has been on identifying fragments of first-order logic sentences for which WFOMC can be computed in time polynomial in the size of the domain. The term coined for this type of tractability by Van den Broeck [2011] is domain liftability. In general, WFOMC and WFOMS are intractable even in this sense already for some sentences from FO3 [12, 9], however, there are non-trivial fragments of first-order logic which have been identified as tractable for WFOMC [13, 11, 14, 15, 16, 6, 17, 18, 19] and for WFOMS [7, 9], including the fragment C2 [6, 10]. 4. Some Applications Here we briefly mention several applications that go beyond the standard machine learning uses of WFOMC and WFOMS. Combinatorics. WFOMC is well-suited for solving problems from enumerative combina- torics.2 The various tractable fragments of WFOMC can be used to count many other non-trivial structures as well, e.g., 𝑘-regular graphs, trees with 𝑘 leaves etc. [3, 17]. The close connection between WFOMC and enumerative combinatorics was used for developing a method capable of generating a database of integer sequences with combinatorial interpretation [4] that we hope could complement the well known OEIS database [21]. Samplers. Standard programming language libraries usually have some support for sampling. For instance, NumPy provides functionality for sampling simple structures such as permutations and combinations. However, when we need to sample a more complex structure, we typically need to develop a sampler from scratch. Having a declarative framework based on WFOMS would be a useful tool for programmers making their work easier. The main reason why there is not such a framework based on the current WFOMS algorithms [9, 10] yet is their practical performance, which is the focus of ongoing works. However, it is worth mentioning that, unsurprisingly, these algorithms already outperform state-of-the-art propositional model samplers on first-order sampling problems, as shown experimentally in [9]. Acknowledgments The author is grateful to the many collaborators who worked on the problems described in this paper (alphabetically): Jáchym Barvínek, Timothy van Bremen, Peter Jung, Martin Svatoš, Jan Tóth, Yuanhong Wang and Yuyi Wang. The work of the author was mainly supported by the Czech Science Foundation projects 20-19104Y, 23-07299S, 24-11820S. 2 There are also other approaches to automating combinatorics within the broader context of lifted inference, most notably [20]. References [1] G. Van den Broeck, N. Taghipour, W. Meert, J. Davis, L. De Raedt, Lifted probabilistic inference by first-order knowledge compilation, in: Proceedings of the Twenty-Second international joint conference on Artificial Intelligence, 2011, pp. 2178–2185. [2] L. Getoor, B. Taskar, Introduction to statistical relational learning, volume 1, MIT press Cambridge, 2007. [3] J. Barvínek, T. van Bremen, Y. Wang, F. Zelezný, O. Kuzelka, Automatic conjecturing of p-recursions using lifted inference, in: Inductive Logic Programming - 30th International Conference, ILP 2021, Proceedings, volume 13191 of Lecture Notes in Computer Science, Springer, 2021, pp. 17–25. URL: https://doi.org/10.1007/978-3-030-97454-1_2. doi:10.1007/ 978-3-030-97454-1\_2. [4] M. Svatoš, P. Jung, J. Tóth, Y. Wang, O. Kuželka, On discovering interesting combinatorial integer sequences, in: Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, 2023. [5] E. Graedel, M. Otto, E. Rosen, Two-variable logic with counting is decidable, in: Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, IEEE, 1997, pp. 306–317. [6] O. Kuželka, Weighted first-order model counting in the two-variable fragment with counting quantifiers, Journal of Artificial Intelligence Research 70 (2021) 1281–1307. [7] Y. Wang, T. van Bremen, Y. Wang, O. Kuželka, Domain-lifted sampling for universal two-variable logic and extensions, in: Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence (AAAI-22), AAAI Press, 2022. [8] M. Richardson, P. Domingos, Markov logic networks, Machine Learning 62 (2006) 107–136. [9] Y. Wang, J. Pu, Y. Wang, O. Kuželka, On exact sampling in the two-variable fragment of first-order logic, in: LICS ’23: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2023. [10] Y. Wang, J. Pu, Y. Wang, O. Kuzelka, Lifted algorithms for symmetric weighted first-order model sampling, Artif. Intell. 331 (2024) 104114. URL: https://doi.org/10.1016/j.artint.2024. 104114. doi:10.1016/J.ARTINT.2024.104114. [11] G. Van den Broeck, On the completeness of first-order knowledge compilation for lifted probabilistic inference, in: Advances in Neural Information Processing Systems, 2011, pp. 1386–1394. [12] P. Beame, G. Van den Broeck, E. Gribkoff, D. Suciu, Symmetric weighted first-order model counting, in: Proceedings of the 34th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, ACM, 2015, pp. 313–328. [13] V. Gogate, P. M. Domingos, Probabilistic theorem proving, in: UAI 2011, Proceedings of the Twenty-Seventh Conference on Uncertainty in Artificial Intelligence, Barcelona, Spain, July 14-17, 2011, 2011, pp. 256–265. [14] G. Van den Broeck, W. Meert, A. Darwiche, Skolemization for weighted first-order model counting, in: Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR), 2014, pp. 1–10. [15] S. M. Kazemi, A. Kimmig, G. V. den Broeck, D. Poole, New liftable classes for first-order probabilistic inference, in: Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems, 2016, pp. 3117–3125. [16] A. Kuusisto, C. Lutz, Weighted model counting beyond two-variable logic, in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, 2018, pp. 619–628. [17] T. Van Bremen, O. Kuželka, Lifted inference with tree axioms, in: Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, 2021, pp. 599–608. [18] J. Tóth, O. Kuželka, Lifted inference with linear order axiom, in: Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI Press, 2023. [19] S. Malhotra, D. Bizzaro, L. Serafini, Lifted inference beyond first-order logic, 2024. arXiv:2308.11738. [20] P. Totis, J. Davis, L. De Raedt, A. Kimmig, Lifted reasoning for combinatorial counting, Journal of Artificial Intelligence Research 76 (2023) 1–58. [21] OEIS Foundation Inc., The on-line encyclopedia of integer sequences, http://oeis.org, 2023. Accessed: 2023-05-01.