The idp system: a model expansion system for an extension of classical logic

Abstract. The model expansion (MX) search problem consists of find-ing models of a given theory T that expand a given finite interpretation. Model expansion in classical first-order logic (FO) has been proposed as the basis for an Answer Set Programming-like declarative programming framework for solving NP problems. In this paper, we present idp, a sys-tem for solving MX problems that integrates technology from ASP and SAT. Its strength lies both in its rich input language and its efficiency. idp is the first model expansion system that can handle full FO, but its language extends FO with many other primitives such as inductive def-initions, aggregates, quantifiers with numerical constraints, order-sorted types, arithmetic, partial functions, etc. We show that this allows for a natural, compact representation of many interesting search problems. Despite the generality of its language, our experiments show that the idp system belongs to the most efficient ASP and MX systems.