Search Problems as Model Finding

ABSTRACT. Arguments for logic-based knowledge representation often emphasize the primacy of entailment in reasoning, and traditional logic-based formulations of AI tasks were frequently in terms of entailment. More recently, practical progress in satisfiability-based methods has encouraged formulation of problems as model finding. Here, we argue for the formalization of search problems, which abound in AI as well as other areas, as a particular form of model finding called model expansion. An important conceptual part of this proposal is the formalization of the problem instance as a struc-ture, rather than as a formula. Adopting this view leads naturally to taking descriptive complexity theory as the starting point for developing a theory of languages for repre-senting search problems. We explain the formalization of search as model expansion, and the reasons we consider it an appropriate basis for such a theory. We emphasize the role of model expansion for first order logic, with extensions, in specifying NP search problems, and describe the formalization of arithmetic in this context. This paper is dedicated to Hector J. Levesque