Satisfiability Checking and Computer Algebra: A Powerful New Search Method

点击翻译按钮获取中文摘要

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.