Solving model expansion tasks: System design and modularity

In this thesis, we present the Enfragmo system for representing and solving combinatorial search problems. The system supports natural specification of problems by providing users with a rich language, based on an extension of first order logic. Since the specification language is high level, Enfragmo provides combinatorial problem-solving capability to users without expertise in advanced solver technology. On the other hand, some search problems, e.g., the task of constructing a logistics service provider relying on local service providers, are inherently modular. The framework is extended to represent a modular system. It allows one to combine modules on an abstract model-theoretic level, independently from what languages are used for describing them. In this thesis, an algorithm for finding solutions to such modular systems is proposed. We show that our algorithm closely corresponds to what is done in practice in different areas such as Satisfiability Modulo Theories, Integer Linear Programming, and Answer Set Programming.