Advancing SAT solving algorithms with Applications to problems in Verification and AI

通过验证和人工智能问题的应用来推进 SAT 求解算法

• 批准号: RGPIN-2016-05527
• 负责人: Bacchus, Fahiem
• 金额: $ 3.35万
• 依托单位: University of Toronto
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2019
• 资助国家: 加拿大
• 起止时间: 2019-01-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=689210
• 关键词: Advancing; SAT; solving; algorithms; Applications

With increasing computing power comes the desire to apply computers to solve ever more complex tasks. Many of these tasks require dealing with problems that are known to be computationally intractable. This means that in the worst case no matter how much computing power we have available to us now or in the future we will not be able to solve such problems. Formally, such problems are characterized as being NP-Hard. ***Nevertheless, recent developments have in practical computing have not been deterred by this worst case analysis. In fact, there are many modern computing applications addressing important practical problems that routinely solve NP-Hard problems. The key this seeming contradiction is that often these practical problems possess extra structure that make them solvable. ***However, except for a few special cases, as yet no one has been able provide an adequate formal characterization of the features that make many practical problems solvable. As a result there are no algorithms for solving such problems with guaranteed reasonable computation times: in order to achieve such guarantees one would need to have a formal characterization of the features that ensure tractability. Instead what has proved to be successful is the development of algorithms for solving the general problem; despite the fact that the general problem is intractable. ***Research over the past 15 years has shown that it is often the case that techniques designed to make an algorithm more effective on the general problem end up being most effective on problems arising from practice; i.e., such techniques tend to be more effective on practical problems. An example of this is the use of clause learning in SAT solvers. ***This observation has motivated much of my previous research and will continue to motivate the research proposed here. In particular, my work has focused on finding techniques and algorithms for solving intractable problems by exploiting ideas designed to make the solver more effective on the general problem. That is, my research has found new algorithms and techniques for building better general purpose solvers and the effect has been that such solvers have been increasingly more effective on a range of important practical problems. ***The proposed research will be to find more effective techniques for solving general purpose problems, specifically MaxSat, #SAT and QBF. Many practical problems can be cast as a MaxSat, #SAT or QBF problem. Hence, once we have an effective solver for these problems we have a method for solving a range of practical problems. ***In addition to this fundamental research into improving solvers for these general problems the proposal is also to apply such solvers to a wider range of practical problems arising in the areas of AI and formal verification. Some work has already been accomplished on this aspect of the research and the proposal involves accomplishing more. **

随着计算能力的增强，人们希望应用计算机来解决越来越复杂的任务。其中许多任务需要处理已知在计算上难以处理的问题。这意味着，在最坏的情况下，无论我们现在或未来拥有多少计算能力，我们都无法解决这些问题。从形式上讲，这类问题的特征是NP-难。*尽管如此，实际计算的最新发展并没有被这一最坏情况分析所吓倒。事实上，有许多现代计算应用程序解决重要的实际问题，这些问题通常解决NP-Hard问题。这种看似矛盾的关键是，这些实际问题往往具有额外的结构，使它们能够得到解决。*然而，除了少数几种特殊情况外，到目前为止还没有人能够对使许多实际问题可以解决的特征提供足够的形式表征。因此，没有算法可以在保证合理计算时间的情况下解决这类问题：为了实现这种保证，需要对确保易处理的特征进行形式化描述。相反，事实证明，成功的是开发了解决一般问题的算法；尽管一般问题是难以解决的。*过去15年的研究表明，通常情况下，旨在使算法在一般问题上更有效的技术最终对实践中出现的问题最有效；即，这种技术在实际问题上往往更有效。这方面的一个例子是在SAT解算器中使用子句学习。*这一观察结果激励了我之前的大部分研究，并将继续激励这里提出的研究。特别是，我的工作重点是通过利用旨在使解算器在一般问题上更有效的想法来寻找解决棘手问题的技术和算法。也就是说，我的研究发现了新的算法和技术，可以构建更好的通用解算器，其效果是，这种解算器在一系列重要的实际问题上越来越有效。*拟议的研究将是寻找更有效的技术来解决一般用途的问题，特别是MaxSat、#SAT和QBF。许多实际问题可以归结为MaxSat、#SAT或QBF问题。因此，一旦我们有了这些问题的有效解决者，我们就有了解决一系列实际问题的方法。*除了这项关于改进这些一般性问题的解算器的基础研究外，提议还将这种解算器应用于人工智能和正式核查领域中出现的更广泛的实际问题。在这方面的研究已经完成了一些工作，建议还需要完成更多的工作。**