Solver Feedback Loops for Automated Constraint Modelling

Imagine assembling a wind turbine: various tasks (e.g. welding two pieces together) must be completed, and the entire assembly must be finished as quickly as possible. Each task has a duration, and some tasks cannot begin until another task is finished. Two tasks using one resource (e.g. a specialised machine) cannot overlap. Project scheduling problems such as this are theoretically hard (NP-complete, in the same class as the Travelling Salesperson Problem) and can be very challenging in practice. Decision problems (such as project scheduling) are pervasive across the public and private sectors and academia.

One way to characterise decision-making and optimization problems is to use a set of decision variables, where each variable represents a choice that must be made to solve the problem. Decision variables are connected by constraints describing the allowed combinations of values. A variable might represent the start time of a task, and a constraint might require one task to end before another task starts.

Powerful solvers have been developed using artificial intelligence and maths to tackle hard decision problems, e.g. the Z3 solver by Microsoft Research. However, these solvers are very sensitive to the way in which a problem is modelled. The model is the set of decision variables and constraints that are used to represent a given problem. Using a poor model can severely hinder the efficiency of a solver, and finding a good model is notoriously difficult even for experts. Therefore, automated modelling is a key research challenge.

We will investigate techniques to improve models automatically, with the overall goal of solving larger and more difficult problems than currently possible. We will exploit solver feedback loops, where a solver is used to derive new information about the problem at hand which is then used to improve the model. Our state-of-the-art modelling tool Savile Row is the ideal platform for this research because it already produces high-quality models for several classes of solver. Our objective is a 10-fold reduction in solving time for hard instances of amenable problem classes.

First, we will research a technique called tabulation. A solver can be inefficient when constraints are not formulated well for it. Tabulation addresses this by replacing existing constraints on a small set of variables with a single constraint that works well with the solver type. The key challenge is to automatically select the sets of variables where tabulation will improve the model. Our early results on automatic tabulation are very promising: solver performance can be increased by hundreds or even thousands of times.

Second, this project will investigate automated modelling for SAT solvers (an extremely efficient type of constraint solver with a basic input language). When targeting SAT, the size of the SAT model is critical to its efficiency. A solver feedback loop can reduce the size by ruling out some combinations of values. Our early work has shown great promise: solver feedback loops can improve SAT solver efficiency by hundreds of times.

Third, we will explore solver feedback loops that use an approximate sampling method to learn facts that are likely to be true in good solutions of the problem at hand. The learned facts can then be used to guide the target solver, enabling it to find good solutions more rapidly.

In addition to advancing knowledge, this project will extend the reach of solvers to solve large and difficult problems. We will engage with potential beneficiaries through open-source software, industry-facing exhibitions, and conferences. With our industry partner IBM, we will apply our research to an important problem: spreadsheet fault localization. We will release a new set of realistic benchmark instances to foster long-term impact. In summary, the project has potential for substantial impact: decision problems are ubiquitous in industry, academia and the public sector.