The complexity of reasoning with FODD and GFODD

Recent work introduced Generalized First Order Decision Diagrams (GFODD) as a knowledge representation language that is useful in mechanizing decision theoretic planning in relational domains. GFODDs generalize function-free first order logic and include numerical values and numerical generalizations of existential and universal quantification. Previous work presented heuristic inference algorithms for GFODDs and implemented these heuristics in systems for decision theoretic planning. In this paper, we study the complexity of the computational problems addressed by such implementations. In particular, we study the evaluation problem, the satisfiability problem, and the equivalence problem for GFODDs under the assumption that the size of the intended model is given with the problem, a restriction that guarantees decidability. Our results provide a complete characterization placing these problems within the polynomial hierarchy. The same characterization applies to the corresponding restriction of problems in first order logic, giving an interesting new avenue for efficient inference when the number of objects is bounded. Our results show that for ΣkΣk formulas, and for corresponding GFODDs, evaluation and satisfiability are ΣkP complete, and equivalence is Πk+1P complete. For ΠkΠk formulas evaluation is ΠkP complete, satisfiability is one level higher and is Σk+1P complete, and equivalence is Πk+1P complete.