Proceedings of the 2nd Workshop on Logic and Search
Knowledge representation, Model generation
The model expansion (MX) search problem consists of finding models of a given theory 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 system for solving MX problems that integrates technology from ASP and SAT. Its strenght 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 definitions, 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.