Arjun：一种高效的独立支持计算技术及其在计数与采样中的应用

给定变量集合 $X$ 上的布尔公式 $\varphi$ 和投影集 $\mathcal{P} \subseteq X$，如果两个解在 $\mathcal{I}$ 上达成一致，则它们在 $\mathcal{P}$ 上也达成一致，那么变量子集 $\mathcal{I}$ 即为 $\mathcal{P}$ 的独立支持。独立支持的概念与可追溯到1901年的经典可定义性概念相关，并已在过去数十年间被研究。最近，确定给定公式的独立支持的计算问题变得重要起来，这是由于独立支持对于基于哈希的计数和采样技术至关重要。在本文中，我们设计了一种高效且可扩展的独立支持计算技术，能够处理源自真实世界基准测试的公式。我们的算法框架名为Arjun，采用了隐式和显式可定义性概念，并基于门识别技术与基于假设的框架的紧密集成。我们证明，使用Arjun增强最先进的模型计数器ApproxMC4和采样器UniGen3可带来显著的性能提升。具体而言，增强后的ApproxMC4在1896个基准中多计数了387个，而增强后的UniGen3在相同时间限制内多采样了319个基准。