A method for solving np search based on model expansion and grounding

摘要

The logical task of model expansion (MX) has been proposed as a declarative constraint programming framework for solving search and decision problems. We present a method for solving NP search problems based on MX for first order logic extended with inductive definitions and cardinality constraints. The method involves grounding, and execution of a propositional solver, such as a SAT solver. Our grounding algorithm applies a generalization of the relational algebra to construct a ground formula representing the solutions to an instance. We demonstrate the practical feasibility of our method with an implementation, called MXG. We present axiomatizations of several NP-complete benchmark problems, and experimental results comparing the performance of MXG with state-of-the-art Answer Set programming (ASP) solvers. The performance of MXG is competitive with, and often better than, the ASP solvers on the problems studied.