An approximative inference method for solving ∃∀SO satisfiability problems

This paper considers the fragment ∃∀SO of second-order logic. Many interesting problems, such as conformantplanning, can be naturally expressed as finite domain satisfiability problems of this logic. Such satisfiability problems are computationally hard and many of these problems are often solved approximately.In this paper, we develop a general approximative method, i.e., a soundbut incomplete method, for solving ∃∀SO satisfiabilityproblems. We use a syntactic representation of a constraintpropagation method for first-order logic to transform such an ∃∀SO satisfiability problem to an ∃SO satisfiabilityproblem (second-order logic, extended with with inductive definitions). The finite domain satisfiability problem for the latterlanguage is in NP and can be handled by several existingsolvers. Next, we look at an extension of first-order logic withinductive definitions (FO(ID)).Inductive definitions are a powerfulknowledge representation tool, and this %motives motivates us to also approximate ∃∀SO(ID) problems. In order to do this, we first show how to perform propagation on such inductive definitions. Next, we use this to approximate ∃∀SO(ID) satisfiability problems. All this provides a general theoretical framework for a number of approximative methods in the literature. Moreover, we also show how we can use this framework for solving practical useful problems, such as conformant planning, in an effective way.status: publishe