Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling

Given a Boolean formula $\\varphi$ over the set of variables $X$ and a\nprojection set $\\mathcal{P} \\subseteq X$, a subset of variables $\\mathcal{I}$\nis independent support of $\\mathcal{P}$ if two solutions agree on\n$\\mathcal{I}$, then they also agree on $\\mathcal{P}$. The notion of independent\nsupport is related to the classical notion of definability dating back to 1901,\nand have been studied over the decades. Recently, the computational problem of\ndetermining independent support for a given formula has attained importance\nowing to the crucial importance of independent support for hashing-based\ncounting and sampling techniques.\n In this paper, we design an efficient and scalable independent support\ncomputation technique that can handle formulas arising from real-world\nbenchmarks. Our algorithmic framework, called Arjun, employs implicit and\nexplicit definability notions, and is based on a tight integration of\ngate-identification techniques and assumption-based framework. We demonstrate\nthat augmenting the state of the art model counter ApproxMC4 and sampler\nUniGen3 with Arjun leads to significant performance improvements. In\nparticular, ApproxMC4 augmented with Arjun counts 387 more benchmarks out of\n1896 while UniGen3 augmented with Arjun samples 319 more benchmarks within the\nsame time limit.\n