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

提案0713499“RI：扩展SAT技术的覆盖范围--量化、计数和抽样”PI：巴特·塞尔曼康奈尔大学摘要许多现实世界的计算问题都需要在一个巨大的潜在解决方案空间中进行搜索。此类问题的例子可以在不同的领域找到，例如在硬件和软件设计和验证、规划和调度以及人工智能(AI)方面。许多这样的问题可以转化为一种常见的表示，称为布尔可满足性(SAT)公式。该公式由一组布尔(True/False)变量和这些变量之间的逻辑约束组成。挑战是找到变量的赋值，使所有约束都得到满足。近年来，我们看到SAT解算器的发展取得了巨大的进步，它寻找令人满意的任务。当前的SAT解算器处理具有100多万个变量和数百万个约束的问题实例。一个耐人寻味的研究问题是，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.