

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.