Reformulations of Constraint Satisfaction Problems : A Survey

Model reformulation plays an important role in improving models, reducing search space so that solutions can be found faster. Hence we categorise model reformulation into three types: a model is reformulated to another model with the same modelling language, a model with non constraint programming standard types is compiled to another model with constraint programming (CP) standard types, and a model is converted to Boolean satisfiability problem (SAT), Mixed-integer programming (MIP), Satisfiability modulo theories (SMT), and Mixed integer linear programming (MILP). Based on these categories, reformulation and compilation could be used in different ways to improve a model such as automatic reformulations, semi-automatic reformulations, MIP to constraint programming, implied constraints, set Constraint Satisfaction Problems (CSPs) to CSPs, string variables to CSP without string variables, symmetry breaking, pre-computation, non-binary to binary translations, and reformulations into SAT, MILP, and SMT. CP is a pervasive and highly successful technology for solving a wide variety of constraint satisfaction problems such as air traffic management, resource allocation, transportation, scheduling, and so on. Model reformulation can have a significant impact on solving time. Techniques from formal methods will be used to provide machine assistance for MiniZinc, which is the high-level modelling language to model CSPs. In this survey, we present an overview of reformulation focusing on the contributions made in the area of reformulation of CSPs where significant performance improvements have been achieved. Our contributions are as follows: propose criteria and types that categorise model reformulations; we systematically unify and organise the vast literature; contrast and compare different categories of the reformulation for solving CSPs; propose a compiler for counter automata reformulation; ultimately, we propose a plan for future work, we identify the challenges, implement frameworks, and evaluate our experimental results of model reformulations