Instance transformation for declarative solvers

Declarative specification-based problem solving systems, or "model-and-solve" systems, solve combinatorial search problems based on specifications in high-level declarative languages. Users of these systems can solve challenging combinatorial problems by describing what a solution is, rather than describing an algorithm for finding one. While the problem specifications are declarative, users of existing systems must write programs to transform problem instances into solver-specific formats, so problem solving is not fully declarative. We describe a purely declarative method for transforming instances from native file formats to solver-specific formats. We also describe a prototype implementation which, used together with existing declarative solvers, provides fully declarative problem solving. The method can also be seen as a way to produce model finders for new logics, of moderate expressive power, purely declaratively. We illustrate application of the method to a variety of problems, including graph problems and logical satisfiability problems.