Solver Feedback Loops for Automated Constraint Modelling

用于自动约束建模的求解器反馈循环

• 批准号: EP/W001977/1
• 负责人: Peter Nightingale
• 金额: $ 39.21万
• 依托单位: University of York
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2022
• 资助国家: 英国
• 起止时间: 2022 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FW001977%2F1
• 关键词: Solver; Feedback; Loops; Automated; Constraint

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.

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