Automated reformulation of specifications by safe delay of constraints

摘要

In this paper we propose a form of reasoning on specifications of combinatorial problems, with the goal of reformulating them so that they are more efficiently solvable. The reformulation technique highlights constraints that can be safely “delayed”, and solved afterwards. Our main contribution is the characterization (with soundness proof) of safe-delay constraints with respect to a criterion on the specification, thus obtaining a mechanism for the automated reformulation of specifications applicable to a great variety of problems, e.g., graph coloring, bin-packing, and job-shop scheduling. This is an advancement with respect to the forms of reasoning done by state-of-the-art-systems, which typically just detect linearity of specifications. Another contribution is an experimentation on the effectiveness of the proposed technique using six different solvers, which reveals promising time savings.