投影模型计数：超越独立支撑集

过去十年见证了投影模型计数实用技术的激增。然而，尽管取得了重大进展，性能扩展仍是该领域的阿喀琉斯之踵。现代计数器使用的一个关键思想是对 \emph{独立支撑集}上的模型进行投影计数，该支撑集通常是投影集（即我们希望投影的原始变量集）的一个小子集。虽然这一思想在提升性能方面行之有效，但能否利用它对投影集之外的变量进行模型投影计数的问题尚未被探索。在本文中，我们研究了这一问题，并表明与直觉相反，对投影集之外的变量进行投影可能是有益的。在二值化神经网络验证、信息流量化、电网可靠性等应用中，投影模型计数的一个良好上界通常就足够了。我们证明，在若干此类情况中，我们可以识别出一组变量，称为上界支撑集（UBS），它不一定是投影集的子集，但对 UBS 投影计数保证能给出真实投影模型计数的上界。从理论上讲，UBS 可以比最小独立支撑集呈指数级缩小。我们的实验表明，即使在其他情况下，基于 UBS 的投影计数也可以比基于独立支撑集的投影计数更高效，同时产生质量非常高的边界。基于广泛的实验，我们发现基于 UBS 的投影计数能够解决许多超出 SOTA 基于独立支撑集的投影模型计数器能力范围的问题实例。