利用维度之利驯服离散积分

离散积分是计算机科学中的一个基本问题，涉及对指数级大集合上的离散和进行计算。尽管三十多年来研究者们兴趣浓厚，但设计可扩展的技术以对离散积分给出具有严格保证的估计仍是圣杯。本工作的关键贡献通过一种将离散积分高效归约为模型计数的方法应对了这一可扩展性挑战。所提出的归约通过显著增加维度来实现，这与传统认知相反，反而转化为求解相对更简单的模型计数问题实例。基于 Chakraborty 等人提出的颇有前景的方法，我们的工作克服了他们方法的关键弱点：仅适用于二进权值。我们用最先进的近似模型计数器增强了所提出的称为 DeWeight 的归约，并对源自神经网络验证领域的基准（一个关键且新兴的应用领域）进行了详细的实证分析。据我们所知，DeWeight 是首个对该类基准计算具有可证明保证的估计的技术。