The Complexity of Reasoning with FODD and GFODD

TL;DR

This paper analyzes the computational complexity of reasoning tasks in GFODDs, a knowledge representation for relational decision making, placing these problems within the polynomial hierarchy and exploring implications for efficient inference.

Contribution

It provides a complete complexity characterization of evaluation, satisfiability, and equivalence problems for GFODDs, extending understanding of their computational boundaries.

Findings

Evaluation and satisfiability are $ ext{Sigma}_k^p$ complete for $ ext{Sigma}_k$ formulas.

Equivalence is $ ext{Pi}_{k+1}^p$ complete for $ ext{Sigma}_k$ formulas.

Complexity results extend to first order logic restrictions with bounded objects.

Abstract

Recent work introduced Generalized First Order Decision Diagrams (GFODD) as a knowledge representation 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 $\Sigma_k$ formulas, and for corresponding GFODDs, evaluation and satisfiability are $\Sigma_k^p$ complete, and equivalence is $\Pi_{k+1}^p$ complete. For $\Pi_k$ formulas evaluation is $\Pi_k^p$ complete, satisfiability is one level higher and is $\Sigma_{k+1}^p$ complete, and equivalence is $\Pi_{k+1}^p$ complete.