SAT and beyond, new algorithms for fundamental reasoning problems

建议的研究将主要集中在开发新的算法和技术，解决可满足性问题及其扩展。在人工智能和计算机科学中，广泛的基础和实际问题可以被视为可满足性（SAT）的实例。这并不奇怪，因为SAT是典型的NP完全问题。令人惊讶的是，尽管它的最坏情况的复杂性，最有效的方法来解决各种实际问题是把他们作为SAT，然后解决所产生的SAT问题与最先进的SAT求解器的状态。例如，硬件验证中的许多问题现在最好使用SAT技术来解决。SAT也有一些有用的概括。两个特别重要的推广是#SAT，计算满意模型的数量的问题，以及QBF（量化布尔公式），它类似于SAT，只是其中一些变量可以普遍量化。这些概括涵盖了更广泛的重要实际问题。例如，贝叶斯网络中的推理问题可以转换为加权的#SAT问题（其中每个满意的模型具有不同的权重）。拟议的研究计划将专注于开发新的和更好的通用算法来解决这些核心可满足性问题：SAT，QBF和#SAT（在其加权和未加权版本）。它将建立在申请人以前的工作。这项先前的工作已经成功地在最先进的技术和我们对这些问题的基本理解方面取得了重大进展。然而，许多重要和微妙的问题仍然存在。解决这些问题将是申请人研究活动的主要重点。这项研究将为培养高素质的人才提供许多机会。

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.