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. We are 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, SkolemFC, that computes an estimate of the number of Skolem functions. 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. Moreover, we show that Skolem function count can be approximated through a polynomial number of calls to a SAT oracle. 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难的；由于即使借助NP预言机，合成单个斯科伦函数仍具有挑战性，因此该问题极不可能存在全多项式随机近似方案（FPRAS）。本研究的主要贡献是提出了首个算法SkolemFC，用于估算斯科伦函数的数量。SkolemFC依赖于计数函数与命题模型计数之间的技术联系：我们的算法对近似模型计数器进行线性次调用，并在理论上保证估算结果。此外，我们证明斯科伦函数计数可通过多项式次SAT预言机调用来近似。我们的原型表现出卓越的可扩展性，即使计算所有此类函数表面上比合成单个函数更具挑战性，其处理基准测试的能力仍可与最先进的斯科伦函数合成引擎相媲美。