RI: Extending the Reach of SAT Technology - Quantification, Counting, and Sampling

提案0713499“RI：扩展SAT技术的范围-量化、计数和采样“PI：BartSelmanCornell大学摘要许多现实世界的计算问题需要在指数级大的潜在解空间中搜索。这些问题的例子可以在不同的领域找到，例如，在硬件和软件设计和验证，规划和调度，以及人工智能（AI）。许多这样的问题可以转化为一个共同的表示，称为布尔可满足性（SAT）公式。该公式由一组布尔（真/假）变量和这些变量之间的逻辑约束组成。挑战是找到一个变量的分配，使所有的约束都得到满足。近年来，我们已经看到了巨大的进步，在发展的SAT求解器，寻找令人满意的分配。目前的SAT求解器处理的问题实例超过一百万个变量和数百万个约束。一个有趣的研究问题是，SAT技术的进步是否可以用于人工智能的其他关键推理任务。该项目考虑了三个这样的任务：（1）量化的布尔推理，多智能体推理和对抗环境中的推理的关键，（2）计算满意任务的数量，这在概率推理中有许多应用，以及（3）从满意任务集中采样，这与模型计数密切相关。该提案的更广泛影响将是设计和开发量化布尔公式（QBF）的有效求解器以及适用于验证，规划，对抗推理和概率推理等领域的广泛用户的模型计数和采样算法。

Proposal 0713499"RI: Extending the Reach of SAT Technology - Quantification, Counting, and Sampling"PI: Bart SelmanCornell UnivsersityABSTRACTMany real-world computational problems require a search through an exponentially large space of potential solutions. Examples of such problems can be found in a diverse range of areas, for example, in hardware and software design and verification, planning and scheduling, and artificial intelligence (AI). Many such problems can be translated into a common representation, called the Boolean Satisfiability (SAT) formulation. This formulation consists of a set of Boolean (True/False) variables and logical constraints among these variables. The challenge is to find an assignment to the variables such that all constraints are satisfied. In recent years, we have seen tremendous progress in the development of SAT solvers, which search for satisfying assignments. Current SAT solvers handle problem instances with over one million variables and several millions of constraints. An intriguing research question is whether the advances in SAT technology can be exploited for other key reasoning tasks central to AI. This project considers three such tasks: (1) quantified Boolean reasoning, key in multi-agent reasoning and reasoning in adversarial settings, (2) counting of the number of satisfying assignments, which has many applications in probabilistic inference, and (3) sampling from the set of satisfying assignments, which is closely related to model counting. The broader impact of the proposal will be the design and development of efficient solvers for quantified Boolean formulas (QBF) and algorithms for model counting and sampling applicable to a wide range of users working in areas as diverse as verification, planning, adversarial reasoning, and probabilistic reasoning.