• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
An Approximate Skolem Function Counter.
Arijit Shaw, Brendan Juba and Kuldeep S. Meel.
In Proceedings of AAAI Conference on Artificial Intelligence (AAAI), January 2024.
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 synthesizing a Skolem function remains challenging, even given access to an NP oracle. The primary contribution of this work is the first algorithm, SkolemFC, that computes 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. 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.
@inproceedings{SJM24,
author={Shaw, Arijit and Juba, Brendan and Meel, Kuldeep S.},
title={An Approximate Skolem Function Counter},
abstract={
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 synthesizing a Skolem function remains challenging, even
given access to an NP oracle. The primary contribution of this work is the
first algorithm, SkolemFC, that computes 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. 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.
},
year={2024},
month=jan,
booktitle=AAAI,
bib2html_pubtype={Refereed Conference},
bib2html_rescat={Counting},
bib2html_dl_pdf={https://ojs.aaai.org/index.php/AAAI/article/view/28650},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21