Compact Propositional Encoding of First-Order Theories

Deepak Ramachandran, Eyal Amir

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|^k\cdot \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.

Content Area: 5. Automated Reasoning

Subjects: 3. Automated Reasoning; 3. Automated Reasoning

Submitted: May 11, 2005

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.