Details of Grant 

EPSRC Reference:	EP/W001977/1
Title:	Solver Feedback Loops for Automated Constraint Modelling
Principal Investigator:	Nightingale, Dr PW
Other Investigators:
Researcher Co-Investigators:
Project Partners:	IBM UK Ltd
Department:	Computer Science
Organisation:	University of York
Scheme:	New Investigator Award
Starts:	01 April 2022	Ends:	03 April 2025	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 (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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic 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