max planck institut
informatik
informatik
Joint work with Deepak Ramachandran (UIUC); some results appeared in AAAI'05.
I will present polynomial-time algorithms that translate First-Order Logic (FOL) theories to smaller propositional encodings than achievable before in polynomial time. For example, we may sometimes reduce the number of propositions to O(|P| + |C|), or O(|P|k * 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, and also on the decidable fragment of the input theory or the use of the Domain Closure Assumption. I will focus on algorithms that accept 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 some verification problems, and we are looking for further applications and challenges in this direction.
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. Our approach scales up inference for many objects, and has potential applications in planning, probabilistic reasoning, and formal verification.