On Knowledge Compilation For Two-Variable First-Order Logic

TL;DR

This paper investigates the feasibility of knowledge compilation for the two-variable fragment of first-order logic, proposing a symmetry-exploiting compiler that improves efficiency in many cases.

Contribution

It introduces a novel two-stage compiler leveraging symmetries in FO2 groundings, enabling more efficient knowledge compilation compared to naive methods.

Findings

Compact compilation is impossible for some FO2 sentences.

The proposed compiler often produces smaller circuits.

Experiments show faster compilation and smaller circuits than baselines.

Abstract

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^{\Omega(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.