Satisfiability Checking and Computer Algebra: A Powerful New Search Method

可满足性检查和计算机代数：一种强大的新搜索方法

• 批准号: RGPIN-2021-03089
• 负责人: Bright, Curtis
• 金额: $ 2.11万
• 依托单位: University of Windsor
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=750342
• 关键词: Satisfiability; Checking; Computer; Algebra; Powerful

Fast search algorithms are at the heart of effective solutions to a huge number of industrial and theoretical problems-from search engines to resource allocation to mathematical conjecture verification. Some of the most effective general-purpose search techniques come from the field of satisfiability (SAT) checking. Indeed, programs called SAT solvers that search for solutions to logic problems are extremely effective at solving many kinds of search and optimization problems that arise in practice-though they tend to struggle with mathematically complex problems. In these kinds of problems it is typical to either use a computer algebra system (CAS) or a "SAT modulo theories" (SMT) solver which offer support for more complex mathematics. However, there are many problems that require both sophisticated mathematics (beyond what SAT or SMT solvers offer) and fast search routines (beyond what CASs offer). This proposal aims to advance a new mathematical search paradigm that exploits both the search power of SAT solvers and the mathematical capabilities of CASs-thereby achieving the best in both the worlds of satisfiability checking and computer algebra. This "SAT+CAS" method is still in its infancy but has shown great promise in a number of preliminary results over the last few years. This research grant will support extending the SAT+CAS method to a wider variety of problems, including those from new kinds of domains. The ultimate goal of this research is to make the SAT+CAS method one of the most effective methods-if not the most effective method-for tackling general mathematical search problems. As one example, consider the problem of testing samples for the presence of a virus. The most basic method is simply to test each sample individually, but this is costly. A more efficient strategy is to employ "pooled testing" where multiple samples are tested together. By judiciously choosing which samples to combine together one can develop testing schemes which are essentially as quick and accurate as the basic method but require significantly fewer tests. For example, disjunct matrices are combinatorial matrices that give rise to good pooling schemes. Optimal disjunct matrices are known to exist once the size of the matrices are large enough, but these can be too large for many applications. However, by extending the SAT+CAS method into the domain of combinatorial group testing we can search for new disjunct matrices-and therefore new pooling schemes. These could be useful to facilitate continuous testing for viruses like COVID-19, especially in regions where the medical system is being pushed to its limits. The SAT+CAS method is perfectly positioned to attack such problems and the time is ripe to exploit the advances made by SAT solvers and CASs in order to solve problems previously considered infeasible.

快速搜索算法是大量工业和理论问题——从搜索引擎到资源分配到数学猜想验证——有效解决方案的核心。一些最有效的通用搜索技术来自可满足性（SAT）检查领域。事实上，被称为SAT解算器的程序在寻找逻辑问题的解决方案时，在解决实践中出现的各种搜索和优化问题方面非常有效——尽管它们往往难以解决数学上复杂的问题。在这类问题中，通常使用计算机代数系统（CAS）或“SAT模理论”（SMT）求解器，它们为更复杂的数学提供支持。然而，有许多问题既需要复杂的数学（超出了SAT或SMT求解器所能提供的），又需要快速的搜索例程（超出了CASs所能提供的）。本提案旨在推进一种新的数学搜索范式，该范式利用了SAT求解器的搜索能力和cas的数学能力，从而在可满足性检查和计算机代数领域都取得了最好的成绩。这种“SAT+CAS”方法仍处于起步阶段，但在过去几年的一些初步结果中显示出很大的希望。这项研究经费将支持将SAT+CAS方法扩展到更广泛的问题，包括来自新领域的问题。本研究的最终目标是使SAT+CAS方法成为解决一般数学搜索问题的最有效方法之一——如果不是最有效的方法的话。作为一个例子，考虑测试样本是否存在病毒的问题。最基本的方法是单独测试每个样品，但这是昂贵的。更有效的策略是采用“池测试”，即多个样本一起测试。通过明智地选择将哪些样品组合在一起，可以开发出本质上与基本方法一样快速和准确的测试方案，但需要的测试次数要少得多。例如，析取矩阵是组合矩阵，可以产生很好的池化方案。当矩阵的大小足够大时，已知存在最优的分离矩阵，但对于许多应用来说，这些矩阵可能太大了。然而，通过将SAT+CAS方法扩展到组合群测试领域，我们可以搜索新的不相交矩阵，从而搜索新的池化方案。这可能有助于促进对COVID-19等病毒的持续检测，特别是在医疗系统已达到极限的地区。SAT+CAS方法完全可以解决这些问题，并且时机已经成熟，可以利用SAT求解器和CAS所取得的进展来解决以前认为不可行的问题。