III: Small: Sampling Techniques in Computational Logic

约束抽样和计数是数据分析中的两个基本问题。在受限抽样中，任务是从布尔公式的可能解中随机抽样。一个相关的问题是约束计数，即确定布尔公式的可能解的数目。这些问题在机器学习、概率推理和规划等领域都有应用，特别是TE项目着眼于电子设计自动化行业，以确定这些问题需要哪些实际解决方案。这两个问题都可以被视为人工智能中最基本的问题之一，即理解给定约束集的解空间结构。本项目专注于基于通用散列的新算法技术的开发，该算法技术是理论计算机科学中的一种经典算法技术。提议的方法背后的许多想法都可以追溯到20世纪80年代，但它们从未被付诸实践。这个项目建立在布尔推理最新进展的基础上，以开发将这些算法想法转化为实践的方法。具有形式保证的近似方法提供了扩展从根本上是一个难以计算的问题的机会。修剪技术也可以减少散列解决方案中的“浪费”，但在确保样本独立分布方面带来了挑战。这项工作有可能在受限采样和计数方面取得突破性结果，为机器学习、概率推理等提供一个新的算法工具箱。

Constrained sampling and counting are two fundamental problems in data analysis. In constrained sampling the task is to sample randomly from among possible solutions to a Boolean formula. A related problem is that of constrained counting, determining the number of possible solutions to a Boolean formula. These problems have applications in machine learning, probabilistic reasoning, and planning, among other areas In particular, te project looks at the electronic-design-automation industry to determine what practical solutions to the problems require. Both problems can be viewed as aspects of one of the most fundamental problems in artificial intelligence, which is to understand the structure of the solution space of a given set of constraints.This project focuses on the development of new algorithmic techniques for constrained sampling and counting, based on a universal hashing - a classical algorithmic technique in theoretical computer science. Many of the ideas underlying the proposed approach go back to the 1980s, but they have never been reduced to practice. This project builds on recent progress in Boolean reasoning to develop methods to reduce these algorithmic ideas to practice. Methods for approximations with formal guarantees provide opportunities to scale what is fundamentally a computationally intractable problem. Pruning techniques can also reduce "waste" in hashed solutions, but introduce challenges in ensuring samples are independently distributed. This work has potential for breakthrough results in constrained sampling and counting, providing a new algorithmic toolbox in machine learning, probabilistic reasoning, and the like.