SAT and beyond, new algorithms for fundamental reasoning problems

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

The proposed research will mainly focus on developing new algorithms and techniques for solving the Satisfiability problem and its extensions. A wide range of fundamental and practical problems in Artificial Intelligence, and in Computer Science in general, can be cast as instances of satisfiability (SAT). This is not surprising since SAT is the canonical NP-Complete problem. What is surprising is that despite its worst case complexity, the most effective way to solve a variety of practical problem is to cast them as SAT and then solve the resulting SAT problem with a state of the art SAT solver. For example, many problems in hardware verification are now best solved using SAT technology. There are also a number of useful generalizations of SAT. Two particularly important generalizations are #SAT, the problem of counting the number of satisfying models, and QBF (Quantified Boolean Formulas), which is like SAT except that some of the variables can be universally quantified. These generalizations cover an even wider range of important practical problems. For example, the problem of inference in Bayesian Networks can be cast as a weighted #SAT problem (where each satisfying model has a different weight). The proposed research program will focus on developing new and better general algorithms for solving these core satisfiability problems: SAT, QBF, and #SAT (in both its weighted and unweighted versions). It will build on previous work by the applicant. This previous work has already been successful in achieving significant advances in the state of the art, and in our fundamental understanding of these problems. Nevertheless many important and subtle problems remain. Addressing these problems will be the main focus of the applicant's research activities. This research will contain many opportunities for the training of highly qualified personnel.