An Approximative Inference Method for Solving ∃ ∀SO Satisfiability Problems

The fragment ∃ ∀ SO(ID) of second order logic extended with inductive definitions is expressive, and many interesting problems, such as conformant planning, can be naturally expressed as finite domain satisfiability problems of this logic. Such satisfiability problems are computationally hard (\(\Sigma^P_2\)). In this paper, we develop an approximate, sound but incomplete method for solving such problems that transforms a ∃ ∀ SO(ID) to a ∃ SO(ID) problem. The finite domain satisfiability problem for the latter language is in NP and can be handled by several existing solvers. We show that this provides an effective method for solving practically useful problems, such as common examples of conformant planning. We also propose a more complete translation to ∃ SO(FP), existential SO extended with nested inductive and coinductive definitions.