Solving NP search problems with model expansion

We explore the application of MXG, a declarative programming solver for NP search problems based on Model Expansion (MX) for first order logic with inductive definitions. We present specifications for several common NP-complete benchmark problems in the language of MXG, and describe some modeling techniques we found useful in obtaining good solver performance. We present an experimental comparison of the performance of MXG with Answer Set Programming (ASP) solvers on these problems, showing that MXG is competitive and often better. As an extended example, we consider an NP-complete phylogenetic inference problem. We present several specifications for this problem, employing a variety of techniques for obtaining good performance. Our best solution, which combines instance pre-processing, redundant axioms, and symmetry breaking axioms, performs orders of magnitude faster than previously reported declarative programming solutions using ASP solvers.