Knowledge compilation transforms logical theories into circuit representations that support efficient reasoning. We study this problem for propositional groundings of FO2, the two-variable fragment of first-order logic over finite domains. Given an FO2 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 FO2 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 FO2 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.

翻译：知识编译将逻辑理论转化为支持高效推理的电路表示。本文针对有限域上二变量一阶逻辑（FO2）的命题层化版本研究该问题。给定一个FO2语句和大小为n的域，其层化产生一个关于地面原子的命题理论。我们研究此类理论是否能在基于DNNF及相关知识编译语言中获得紧凑表示，以及这些表示能否针对固定语句的域规模n被高效构建。首先证明紧凑编译在一般情况下不可行：存在一个FO2语句，其在大小为n的域上的层化需要$2^{Ω(n)}$大小的DNNF。在正面结果方面，我们开发了一个两阶段编译器，利用FO2语句命题层化中固有的对称性。该编译器在分支时基于一元和二元类型而非单个地面原子，其思路类似于概率关系模型中的提升推理。此外，通过高效识别并缓存与未来扩展等价的残余子问题，优化了编译过程。实验表明该方法具有实际效率，通常比直接的基于层化的基线方法生成更小的电路且编译速度更快。