Grounding for Model Expansion in k-Guarded Formulas with Inductive Definitions

Abstract

Mitchell and Ternovska proposed a constraint programming framework based on classical logic extended with inductive definitions. They formulate a search problem as the problem of model expansion (MX), which is the problem of expanding a given structure with new relations so that it satisfies a given formula. Their long-term goal is to produce practical tools to solve combinatorial search problems, especially those in NP. In this framework, a problem is encoded in a logic, an instance of the problem is represented by a finite structure, and a solver generates solutions to the problem. This approach relies on propositionalisation of high-level specifications, and on the efficiency of modern SAT solvers. Here, we propose an efficient algorithm which combines grounding with partial evaluation. Since the MX framework is based on classical logic, we are able to take advantage of known results for the so-called guarded fragments. In the case of k-guarded formulas with inductive definitions under a natural restriction, the algorithm performs much better than naive grounding by relying on connections between k-guarded formulas and tree decompositions.