Given a Boolean formula $\varphi$ over the set of variables $X$ and a projection set $\mathcal{P} \subseteq X$, a subset of variables $\mathcal{I}$ is independent support of $\mathcal{P}$ if two solutions agree on $\mathcal{I}$, then they also agree on $\mathcal{P}$. The notion of independent support is related to the classical notion of definability dating back to 1901, and have been studied over the decades. Recently, the computational problem of determining independent support for a given formula has attained importance owing to the crucial importance of independent support for hashing-based counting and sampling techniques. In this paper, we design an efficient and scalable independent support computation technique that can handle formulas arising from real-world benchmarks. Our algorithmic framework, called Arjun, employs implicit and explicit definability notions, and is based on a tight integration of gate-identification techniques and assumption-based framework. We demonstrate that augmenting the state of the art model counter ApproxMC4 and sampler UniGen3 with Arjun leads to significant performance improvements. In particular, ApproxMC4 augmented with Arjun counts 387 more benchmarks out of 1896 while UniGen3 augmented with Arjun samples 319 more benchmarks within the same time limit.
翻译:鉴于Boolean公式在一组变量(X$)和预测值($mathcal{P})中的美元,一个变量的子集($mathcal{I})是美元(mathcal{P}美元)的独立支持,如果两个解决方案同意美元(mathcal{I}美元),那么他们也同意美元(mathcal{P}美元)。独立支持的概念与1901年前的典型定义概念有关,并经过数十年的研究。最近,确定对某一公式的独立支持的计算问题已经变得重要,因为独立支持基于散列的计数和取样技术至关重要。在本文件中,我们设计了一个高效和可扩缩的独立支持计算技术,可以处理来自真实世界基准的公式。我们的算法框架叫做Arjun,采用隐含和明确的可定义概念,并且基于严格整合了门级识别技术和假设框架。我们证明,将艺术模型(AgrosMC4) 独立支持一个计算问题提升状态,而AgroxMC4 和Arjun 更大规模地改进了Arjun ALG3的测试基准。