On Knowledge Compilation For Two-Variable First-Order Logic
For researchers in knowledge compilation and lifted inference, this work provides both a fundamental lower bound and a practical compiler for FO2 groundings, though the problem is inherently hard.
The paper studies knowledge compilation for propositional groundings of two-variable first-order logic (FO2) over finite domains. It proves that compact DNNF representations are impossible in general (exponential lower bound), but introduces a two-stage compiler exploiting symmetries that often produces smaller circuits and compiles faster than baselines.
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.