Solver Feedback Loops for Automated Constraint Modelling

想象一下组装一台风力涡轮机：必须完成各种任务(例如，将两个部件焊接在一起)，并且必须尽快完成整个组装。每个任务都有工期，有些任务只有在另一个任务完成后才能开始。使用同一资源(例如，专用机器)的两个任务不能重叠。像这样的项目调度问题在理论上是困难的(NP-完全，与旅行推销员问题属于同一类)，并且在实践中可能非常具有挑战性。决策问题(如项目日程安排)普遍存在于公共和私营部门以及学术界。描述决策和优化问题的一种方法是使用一组决策变量，其中每个变量代表解决问题所必须做出的选择。决策变量通过描述允许的值组合的约束来连接。变量可能表示任务的开始时间，而约束可能要求一个任务在另一个任务开始之前结束。使用人工智能和数学开发了强大的解算器来解决困难的决策问题，例如微软研究院的Z3解算器。然而，这些解算器对问题建模的方式非常敏感。该模型是用于表示给定问题的决策变量和约束的集合。使用一个糟糕的模型会严重阻碍求解器的效率，而且即使对专家来说，找到一个好的模型也是出了名的困难。因此，自动化建模是一个关键的研究挑战。我们将研究自动改进模型的技术，总体目标是解决比目前可能的更大、更难的问题。我们将利用求解器反馈循环，其中求解器被用来获得关于手头问题的新信息，然后这些信息被用来改进模型。我们最先进的建模工具Savile Row是这项研究的理想平台，因为它已经为几类求解器生成了高质量的模型。我们的目标是将可服从问题类的困难实例的解决时间减少10倍。首先，我们将研究一种名为制表的技术。当没有很好地为求解器制定约束时，求解器可能会效率低下。制表通过将一小部分变量上的现有约束替换为与求解器类型配合良好的单个约束来解决这一问题。关键的挑战是自动选择制表将改进模型的变量集。我们在自动制表方面的早期结果非常有希望：求解器的性能可以提高数百甚至数千倍。其次，这个项目将研究SAT解算器(一种使用BASIC输入语言的极其高效的约束解算器)的自动建模。当以SAT为目标时，SAT模型的大小对其效率至关重要。求解器反馈循环可以通过排除某些值组合来减小大小。我们的早期工作显示出巨大的希望：求解器反馈循环可以将SAT求解器的效率提高数百倍。第三，我们将探索解算器反馈循环，它使用近似抽样方法来学习在手头问题的良好解决方案中可能是正确的事实。学习到的事实可以用来指导目标解算器，使其能够更快地找到好的解决方案。除了推进知识，这个项目将扩大解决者的触角，以解决大型和困难的问题。我们将通过开源软件、面向行业的展览和会议与潜在受益者接触。与我们的行业合作伙伴IBM一起，我们将把我们的研究应用到一个重要的问题上：电子表格故障定位。我们将发布一套新的现实基准实例，以培育长期影响。总而言之，该项目有可能产生重大影响：决策问题在工业界、学术界和公共部门无处不在。

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.