EPSRC Reference: 
EP/W001977/1 
Title: 
Solver Feedback Loops for Automated Constraint Modelling 
Principal Investigator: 
Nightingale, Dr PW 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science 
Organisation: 
University of York 
Scheme: 
New Investigator Award 
Starts: 
01 November 2021 
Ends: 
30 April 2024 
Value (£): 
307,728

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
13 Sep 2021

EPSRC ICT Prioritisation Panel September 2021

Announced


Summary on Grant Application Form 
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 (NPcomplete, 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 decisionmaking 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 stateoftheart modelling tool Savile Row is the ideal platform for this research because it already produces highquality models for several classes of solver. Our objective is a 10fold 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 opensource software, industryfacing 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 longterm impact. In summary, the project has potential for substantial impact: decision problems are ubiquitous in industry, academia and the public sector.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.york.ac.uk 