Automatic Core-Guided Reformulation via Constraint Explanation and Condition Learning

SAT and propagation solvers often underperform for optimisation models whose objective sums many single-variable terms. MaxSAT solvers avoid this by detecting and exploiting cores: subsets of these terms that cannot jointly take their lower bounds. Previous work demonstrated that manual analysis of cores can help define model reformulations likely to speed up solving for many model instances. This paper presents a method to automate this process. For each selected core the method identifies the instance constraints that caused it; infers the model constraints and parameters that explain how these instance constraints were formed; and learns the conditions that made those model constraints generate cores, while others did not. It then uses this information to reformulate the objective. The empirical evaluation shows this method can produce useful reformulations. Importantly, the method can be useful in other situations that require explaining a set of constraints.

Combinatorial problems are often tackled using a mod-elling+solving approach, whose first step is to model the problem's parameters, variables, constraints and objective function (if any) using a modelling language such as AMPL (Fourer, Gay, and Kernighan 1987), OPL (Van Hentenryck 1999), Essence (Frisch et al. 2007) or MINIZ-INC (Nethercote et al. 2007). Each instantiation of the model parameters with input data yields a model instance, which is then compiled to the format required by the selected solver to find its solutions. This compilation step uses sophisticated methods to generate a flattened instance (often written in a leaner formalism such as Essence' (Rendl 2010) and FLATZINC (Nethercote et al. 2007)) that is no longer intuitive for humans but is efficient for the selected solver. This approach gives users expressive and intuitive languages to model their problems, and frees them from knowing how to best map models onto solving algorithms. Further, modelto-model transformation methods exist to improve a model for many/all its instances, rather than just the one being flattened (e.g., (