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

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

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.