This paper introduces a new perspective on model counting in Boolean satisfiability (#SAT), focusing on how much information about the distribution of solutions can be extracted through a limited number of counting experiments. Given a fixed set of variables, each satisfying assignment of a formula induces a local pattern. Instead of computing the total number of solutions, we study how to recover statistical information about these local patterns using controlled extensions of the formula, called probes. Each probe slightly modifies the formula and reveals information through the change in the number of solutions. The paper develops a formal framework for this idea and introduces the notion of probe complexity, which measures the minimum number of probes required to determine a given local statistic. We show that this complexity depends exactly on the number of independent components of the statistic. This leads to precise results for several natural quantities, including variable bias, equality relations, parity, and full local distributions. We also study a different task: guaranteeing that the number of solutions strictly increases, regardless of the formula. Surprisingly, we show that a single probe is never sufficient, while two probes always suffice. A second part of the paper investigates what happens when probes must be implemented using explicit CNF formulas under structural constraints. In this setting, we introduce realizable probe complexity and show that structural restrictions can increase the probing cost. In particular, for parity, we prove a strict separation between the ideal (abstract) setting and the realizable one. These results suggest a new structural viewpoint on model counting, separating the intrinsic informational content of local statistics from the constraints imposed by concrete logical representations.
Fabrizio De Palma (Sat,) studied this question.