Compact Propositional Encoding of First-Order Theories

                                     Eyal Amir
                       Computer Science Department
                 University of Illinois, Urbana-Champaign
                        http://www.cs.uiuc.edu/~eyal

Joint work with Deepak Ramachandran

A common solution to inference and decision problems is first to
represent them in a subset of First-Order Logic (FOL) and then to
translate them to propositional logic for efficient solution (e.g.,
using a SAT solver). However, standard translation techniques result
in very large propositional encodings ($O(|P||C|^k)$ for $|P|$
predicates of arity $k$ and $|C|$ constant symbols) that are often
infeasible to solve. They also require semantic assumptions (e.g.,
enumeration of objects) for correctness.
 
In this talk I present polynomial-time algorithms that translate FOL
theories to smaller propositional encodings than achievable before
($O(|P|+|C|)$), if the FOL representation has some local
structure. Our algorithms accept broad classes of FOL theories,
preserve soundness and completeness, and do not require assumptions on
the number or identity of objects. Our experimental results confirm
the theoretical promise and show significant speedup of inference with
a SAT solver. This approach scales up inference to many objects, and
it is promissing for other applications, such as planning,
probabilistic reasoning, and formal verification.