Knowledge compilation transforms logical theories into circuit representations that support efficient reasoning. We study this problem for propositional groundings of FO², the two-variable fragment of first-order logic over finite domains. Given an FO² sentence and a domain of size n, its grounding yields a propositional theory over ground atoms. We ask whether such theories admit compact representations in DNNF-based and related knowledge compilation languages, and whether these can be constructed efficiently, both with respect to the domain size n for a fixed sentence. We show first that compact compilation is impossible in general: there exists an FO² sentence whose grounding over a domain of size n requires DNNF size 2^Ω(n). On the positive side, we develop a two-stage compiler that exploits the symmetries inherent in the propositional groundings of FO² sentences. It branches on unary and binary types rather than individual ground atoms, in a similar spirit to lifted inferences for probabilistic relational models. Moreover, it optimizes the compilation process by efficiently identifying and caching residual subproblems that are equivalent with respect to future extensions. Experiments show the practical efficiency of our approach, which often produces smaller circuits and compiles faster than straightforward grounding-based baselines.

We study the model enumeration problem of the function-free, finite domain fragment of first-order logic with two variables (FO2). Specifically, given an FO2sentence Γ and a positive integer n, how can one enumerate all the models of Γ over a domain of size n? In this paper, we devise a novel algorithm to address this problem. The delay complexity, the time required between producing two consecutive models, of our algorithm is quadratic in the given domain size n (up to logarithmic factors) when the sentence is fixed. This complexity is almost optimal since the interpretation of binary predicates in any model requires at least Ω(n2) bits to represent.

We consider the task of weighted first-order model counting (WFOMC), a fundamental problem of probabilistic inference in statistical relational learning. The goal of WFOMC is to compute the weighted sum of models of a given first-order logic sentence over a finite domain, where each model is assigned a weight by a pair of weighting functions. Past work has shown that WFOMC can be solved in polynomial time in the domain size if the sentence is in the two-variable fragment of first-order logic (FO2). This result is later extended to the case where the sentence is in FO2with the linear order axiom, which requires a binary predicate in the sentence to introduce a linear ordering of the domain elements. However, despite its polynomial theoretical complexity, the existing domain-liftable algorithm for WFOMC with the linear order often suffers from inefficiencies when applied to real-world problems. This paper introduces a novel domain-lifted algorithm for WFOMC with the linear order axiom. Compared to the existing approach, our proposed algorithm exploits the inherent symmetries within first-order logic sentences and weighting functions to minimize redundant computations. Experimental results verify the efficiency of our approach, demonstrating a significant speedup over the existing approach.