One approach to probabilistic inference involves counting the number of models of a given Boolean formula. Here, we are interested in inferences involving higher-order objects, i.e., functions. We study the following task: Given a Boolean specification between a set of inputs and outputs, count the number of functions of inputs such that the specification is met. Such functions are called Skolem functions. Our study is motivated by the recent development of scalable approaches to Boolean function synthesis. This stands in relation to our problem analogously to the relationship between Boolean satisfiability and the model counting problem. Yet, counting Skolem functions poses considerable new challenges. From the complexity-theoretic standpoint, counting Skolem functions is not only $\#P$-hard; it is quite unlikely to have an FPRAS (Fully Polynomial Randomized Approximation Scheme) as the problem of even synthesizing one Skolem function remains challenging, even given access to an NP oracle. The primary contribution of this work is the first algorithm, $\mathsf{SkolemFC}$, that computes the number of Skolem functions. $\mathsf{SkolemFC}$ relies on technical connections between counting functions and propositional model counting: our algorithm makes a linear number of calls to an approximate model counter and computes an estimate of the number of Skolem functions with theoretical guarantees. Our prototype displays impressive scalability, handling benchmarks comparably to state-of-the-art Skolem function synthesis engines, even though counting all such functions ostensibly poses a greater challenge than synthesizing a single function.

翻译：概率推理的一种方法涉及计算给定布尔公式的模型数量。在此，我们关注涉及高阶对象（即函数）的推理。我们研究以下任务：给定输入与输出之间的布尔规范，计算满足该规范的输入函数数量。此类函数被称为斯科伦函数。我们的研究受到近期布尔函数合成可扩展方法发展的启发。这类似于布尔可满足性问题与模型计数问题之间的关系。然而，计数斯科伦函数带来了全新的挑战。从计算复杂性角度而言，计数斯科伦函数不仅是$\#P$-难的，甚至不太可能存在FPRAS（完全多项式随机近似方案），因为即使调用NP预言机，合成单个斯科伦函数仍然具有挑战性。本研究的主要贡献是提出了首个计算斯科伦函数数量的算法$\mathsf{SkolemFC}$。$\mathsf{SkolemFC}$依赖于计数函数与命题模型计数之间的技术关联：该算法对近似模型计数器进行线性次调用，并在理论保证下估计斯科伦函数的数量。我们的原型展现出惊人的可扩展性，其性能可媲美最先进的斯科伦函数合成引擎，尽管计数所有此类函数表面上比合成单个函数更具挑战性。