Compact Propositional Encodings of First-Order Theories

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 20

Automated Reasoning

In this paper we present polynomial-time algorithms that translate First-Order Logic (FOL) theories to smaller propositional encodings than achievable before in polynomial time. For example, we can sometimes reduce the number of propositions to $O(|P|+|C|)$, or $O(|P|^kcdot log |P|)$, for $|P|$ predicates of arity $k$ and $|C|$ constant symbols. The guarantee depends on availability of some graphical structure in the FOL representation. Our algorithms accept all FOL theories, and preserve soundness and completeness (sometimes requiring the Domain Closure Assumption). Our experiments show significant speedup in inference with a SAT solver on real-world problems. Our results address a common approach that translates inference and decision problems that originate in FOL into propositional logic, later applying efficient SAT solvers. Standard translation techniques result in very large propositional encodings ($O(|P||C|^k)$ for predicates of arity $k$) that are often infeasible to solve. This approach scales up inference for many objects, and has potential applications in planning, probabilistic reasoning and formal verification.