Abstract
Many synthesis problems can be solved by formulating them as a quantified Boolean formulas (QBF). For such problems, a mere true/false answer is often inadequate. Instead, it is necessary to express the answer in terms of Skolem functions reflecting the quantifier dependencies of the variables. In this work, we consider a quantitative variant of the problem, counting the number of Skolem functions. This problem arises in practical settings, such as program verification and evaluation of specifications. 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 a FPRAS as the problem of even synthesizing one Skolem function remains challenging, even given an NP oracle. Nevertheless, in this work we propose an algorithm for the problem, as well as a corresponding implementation, that employs a exact model counter for a linear number of #SAT queries, and produces the approximate number of Skolem functions with PAC guarantees. Our tool scales to formulas with thousands of variables. Based on joint work with Kuldeep Meel and Arijit Shaw.