# An Approximate Skolem Function Counter

Arijit Shaw,1,2 Brendan Juba,3 Kuldeep S. Meel4

###### 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.

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.

##  1 Introduction

Probabilistic inference problems arise throughout AI and are tackled
algorithmically by casting them as problems such as model counting (Gomes,
Sabharwal, and Selman 2021; Chakraborty, Meel, and Vardi 2021). In this work,
we are interested in approaching inference questions for higher-order objects,
specifically _Skolem functions_ : that is, towards solving inference tasks, we
wish to compute the number of possible Skolem functions for a given
specification $F(X,Y)$. Counting Skolem functions is the natural analog of
$\\#SAT$ for Skolem functions, yet to our knowledge, it has not been
previously studied.

More precisely, recall that given two sets $X=\\{x_{1},\dots,x_{n}\\}$ and
$Y=\\{y_{1},\dots,y_{m}\\}$ of variables and a Boolean formula $F(X,Y)$ over
$X\cup Y$, the problem of Boolean functional synthesis is to compute a vector
$\Psi=\langle\psi_{1},\dots,\psi_{m}\rangle$ of Boolean functions $\psi_{i}$,
often called Skolem functions, such that $\exists YF(X,Y)\equiv F(X,\Psi(X))$.
Informally, given a specification between inputs and outputs, the task is to
synthesize a function vector $\Psi$ that maps each assignment of the inputs to
an assignment of the outputs so that the combined assignment meets the
specification (whenever such an assignment exists). Skolem synthesis is a
fundamental problem in formal methods and has been investigated by
theoreticians and practitioners alike over the last decade. The past few years
have witnessed the development of techniques that showcase the promise of
scalability in their ability to handle challenging specifications (Rabe et al.
2018; Jiang, Lin, and Hung 2009; Tabajara and Vardi 2017; Akshay et al. 2019;
Golia et al. 2021).

The scalability of today’s Skolem synthesis engines is reminiscent of the
scalability of SAT solvers in the early 2000s. Motivated by the scalability of
SAT solvers (Froleyks et al. 2021), researchers sought algorithmic frameworks
for problems beyond satisfiability, such as MaxSAT (Ansótegui, Bonet, and Levy
2013; Li and Manya 2021), model counting (Gomes, Sabharwal, and Selman 2021;
Chakraborty, Meel, and Vardi 2021), sampling (Chakraborty, Meel, and Vardi
2014), and the like. The development of scalable techniques for these problems
also helped usher in new applications, even though the initial investigation
had not envisioned many of these applications. In a similar vein, motivated in
part by this development of scalable techniques for functional synthesis, we
investigate the Skolem counting problem. We observe in Section 1.2 that
algorithms for such tasks also have potential applications in security and the
engineering of specifications. Being a natural problem, we will see that our
study also naturally leads to deep technical connections between counting
functions and counting propositional models and the development of new
techniques, which is of independent interest.

Counting Skolem functions indeed raises new technical challenges. The existing
techniques developed in the context of propositional model counting either
construct (implicitly or explicitly) a representation of the space of all
models (Thurley 2006; Dudek, Phan, and Vardi 2020; Sharma et al. 2019) or at
least enumerate a small number of models (Chakraborty, Meel, and Vardi 2013,
2016) (which in practice amounts to a few tens to hundreds of models) of
formulas constrained by random XORs. Such approaches are unlikely to work in
the context of Skolem function counting, where even finding one Skolem
function is hard, and there are no techniques that enable the enumeration of
Skolem functions.

###  1.1 Technical Contribution

The primary contribution of this work is the development of a novel
algorithmic framework, called $\mathsf{SkolemFC}$, that approximates the
Skolem function count with a theoretical guarantee, using only linearly many
calls to an approximate model counter and sampler. First, we identify that
Skolem function counting can be reduced exponential number of model counting
calls, serving as a baseline Skolem function counter. The core technical idea
of $\mathsf{SkolemFC}$ is to reduce the problem of approximate Skolem function
counting to only linearly many (in $m=|Y|$) calls to propositional model
counters. Of particular note is the observation that $\mathsf{SkolemFC}$ can
provide an approximation to the number of Skolem functions without enumerating
even one Skolem function.

To measure the impact of the algorithm, we implement $\mathsf{SkolemFC}$ and
demonstrate its potential over a set of benchmarks arising from prior studies
in the context of Skolem function synthesis. Out of 609 instances,
$\mathsf{SkolemFC}$ could solve 379 instances, while a baseline solver could
solve only eight instances. For context, the state-of-the-art Skolem function
synthesis tool $\mathsf{Manthan}$$\mathsf{2}$ (Golia et al. 2021) effectively
tackled 509 instances from these benchmarks, while its precursor,
$\mathsf{Manthan}$ (Golia, Roy, and Meel 2020), managed only 356 instances
with a timeout of 7200 seconds. This accomplishment is particularly
significant because it demonstrates that addressing a quantitative issue at a
scale comparable to that of a synthesis engine represents a significant leap
forward in the field.

###  1.2 Applications

This problem arises in several potential application areas.

#### Specification engineering.

The first and primary motivation stems from the observation that specification
synthesis (Albarghouthi, Dillig, and Gurfinkel 2016; Prabhu et al. 2021)
(i.e., the process of constructing $F(X,Y)$) and function synthesis form part
of the iterative process wherein one iteratively modifies specifications based
on the functions that are constructed by the underlying engine. In this
context, one helpful measure is to determine the number of possible
semantically different functions that satisfy the specification, as often a
large number of possible Skolem functions indicates the vagueness of
specifications and highlights the need for strengthening the specification.

#### Diversity at the specification level.

In system security and reliability, a classic technique is to generate and use
a diverse variety of functionally equivalent implementations of components
(Baudry and Monperrus 2015). Although classically, this is achieved by
transformations of the code that preserve the function computed, we may also
be interested in producing a variety of functions that satisfy a common
specification. Unlike transformations on the code, it is not immediately clear
whether a specification even admits a diverse collection of functions –
indeed, the function may be uniquely defined. Thus, counting the number of
such functions is necessary to assess the potential value of taking this
approach. Approximate counting of the functions may also be a useful primitive
for realizing such an approach.

#### Uninterpreted functions in SMT.

A major challenge in the design of counting techniques for SMT (Chistikov,
Dimitrova, and Majumdar 2015; Chakraborty et al. 2016) lies in handling
uninterpreted functions (Kroening and Strichman 2016). Since Skolem functions
capture a restricted but large enough class of uninterpreted functions
(namely, the case where a given uninterpreted function is allowed to depend on
all $X$ variables), progress in Skolem function counting is needed if we hope
to make progress on the general problem of counting of uninterpreted functions
in SMT.

#### Evaluation of a random Skolem function.

Although synthesis of Skolem functions remains challenging in general, we note
that approximate counting enables a kind of incremental evaluation by using
the standard techniques for reducing sampling to counting. More concretely,
given a query input, we can estimate the number of functions that produce each
output: this is trivial if the range is small (e.g., Boolean), and otherwise,
we can introduce random XOR constraints to incrementally specify the output.
Once an output is specified for the query point, we may retain these
constraints when estimating the number of consistent functions for subsequent
queries, thereby obtaining an approximately uniform function conditioned on
the answers to the previous queries.

_Organization._ The rest of the paper is organized as follows: we discuss
related work in Section 2 and present notation and preliminaries in Section 3.
We then present the primary technical contribution of our work in Section 4.
We present the empirical analysis of the prototype implementation of
$\mathsf{SkolemFC}$ in Section 5. We finally conclude in Section 6.

##  2 Related Work

Despite the lack of prior studies focused on the specific problem of counting
Skolem functions, significant progress has been made in synthesizing these
functions. Numerous lines of research have emerged in the field of Skolem
function synthesis. The first, incremental determinization, iteratively
pinpoints variables with distinctive Skolem functions, making decisions on any
remaining variables by adding provisional clauses that render them
deterministic (Rabe 2019; Rabe and Seshia 2016; Rabe et al. 2018). The second
line of research involves obtaining Skolem functions by eliminating
quantifiers using functional composition and reducing the size of composite
functions through the application of Craig interpolation (Jiang, Lin, and Hung
2009; Jiang 2009). The third, CEGAR-style approaches, commence with an initial
set of approximate Skolem functions, and proceed to a phase of counter-example
guided refinement to improve upon these candidate functions (John et al. 2015;
Akshay et al. 2017, 2018). Work on the representation of specification
$F(X,Y)$ has led to efficient synthesis using ROBDD representation and
functional composition (Balabanov and Jiang 2011), with extensions to factored
specifications (Tabajara and Vardi 2017; Chakraborty et al. 2018). Notable
advancements include the new negation normal form, SynNNF, amenable to
functional synthesis (Akshay et al. 2019). Finally, a data-driven method has
arisen (Golia, Roy, and Meel 2020; Golia et al. 2021), relying on constrained
sampling to generate satisfying assignments for a formula $F$. These
assignments are fed into a decision-tree learning technique, allowing the
creation of Skolem functions.

A related problem in the descriptive complexity of functions definable by
counting the Skolem functions for _fixed_ formulas have been shown to
characterize $\\#AC_{0}$ (Haak and Vollmer 2019). By contrast, we are
interested in the problem where the _formula_ is the input. Our algorithm also
bears similarity to the FPRAS proposed for the descriptive complexity class
$\\#\Sigma_{1}$ (Durand et al. 2021), which is obtained by an FPRAS for
counting the number of _functions_ satisfying a DNF over atomic formulas
specifying that the functions must/must not take specific values at specific
points. Nevertheless, our problem is fundamentally different in that it is
easy to find functions satisfying such DNFs, whereas synthesis of Skolem
functions is unlikely to be possible in polynomial time.

The specifications for the functions are often expressed in terms of
quantified Boolean formulas (QBFs). In context of QBF, a different
quantitative question has been addressed. AllQBF (Becker et al. 2012) is task
to find all assignments of free variables occurring in a given QBF such that
the formula evaluates to true. CountingQBF (Shukla et al. 2022) poses a
similar query within a quantitative aspect. However, their relevance to the
counting functions isn’t directly apparent, and it’s uncertain whether they
can be adapted for function counting purposes.

##  3 Notation and Preliminaries

We use lowercase letters (with subscripts) to denote propositional variables
and uppercase letters to denote a subset of variables. The formula $\exists
YF(X,Y)$ is existentially quantified in $Y$ , where
$X=\\{x_{1},\dots,x_{n}\\}$ and $Y=\\{y_{1},\dots,y_{m}\\}$. By $n$ and $m$ we
denote the number of $X$ and $Y$ variables in the formula. Therefore,
$n=|X|,m=|Y|$. For simplicity, we write a formula $F(X,Y)$ as $F$ if the $X,Y$
is clear from the context. A _model_ is an assignment (true or false) to all
the variables in $F$, such that $F$ evaluates to true. Let
$\mathsf{Sol}(F)_{\downarrow{S}}$ denote the set of models of formula $F$
projected on $S\subseteq X\cup Y$. If $S=X\cup Y$, we write the set as
$\mathsf{Sol}(F)$. Let $\sigma$ be a partial assignment for the variables $X$
of $F$. Then $\mathsf{Sol}(F\wedge(X=\sigma))$ denotes subset of models of
$F$, where $X=\sigma$.

#### Propositional Model Counting.

Given a formula $F$ and a projection set $S$, the problem of model counting is
to compute $|\mathsf{Sol}(F)_{\downarrow{S}}|$. An _approximate model counter_
takes in a formula $F$, projection set $S$, tolerance parameter $\varepsilon$,
confidence parameter $\delta$ and returns $c$ such that
$\Pr\left[\frac{|\mathsf{Sol}(F)_{\downarrow{S}}|}{1+\varepsilon}\leq
c\leq(1+\varepsilon)|\mathsf{Sol}(F)_{\downarrow{S}}|\right]\geq 1-\delta$.

#### Propositional Sampling.

Given a Boolean formula $F$ and a projection set $S$, a _sampler_ is a
probabilistic algorithm that generates a random element in
$\mathsf{Sol}(F)_{\downarrow{S}}$. An _almost uniform sampler_ $G$ inputs a
tolerance parameter $\varepsilon$ along with $F$ and $S$, and guarantees
$\forall
y\in\mathsf{Sol}(F)_{\downarrow{S}},\frac{1}{(1+\varepsilon)|\mathsf{Sol}(F)_{\downarrow{S}}|}\leq\Pr[G(F,S,\varepsilon)=y]\leq\frac{(1+\varepsilon)}{|\mathsf{Sol}(F)_{\downarrow{S}}|}$.

#### Skolem Function.

Given a Boolean specification $F(X,Y)$ between set of inputs
$X=\\{x_{1},\dots,x_{n}\\}$ and vector of outputs $Y=\langle
y_{1},\dots,y_{m}\rangle$, a function vector
$\Psi(X)=\langle\psi_{1}(X),\psi_{2}(X),\dots,\psi_{m}(X)\rangle$ is a Skolem
function vector if $y_{i}\leftrightarrow\psi_{i}(X)$ and $\exists
YF(X,Y)\equiv F(X,\Psi)$. We refer to $\Psi$ as the Skolem function vector and
$\Psi_{i}$ as the Skolem function for $y_{i}$. We’ll use the notation
$\mathsf{Skolem}(F,Y)$ to denote the set of possible $\Psi(X)$ satisfying the
condition $\exists YF(X,Y)\equiv F(X,\Psi(X))$. Two Skolem function vectors
$\Psi_{1},\Psi_{2}$ are different, if there exist an assignment $\sigma$ for
variable $X$, for which $\Psi_{1}(\sigma),\Psi_{2}(\sigma)$ differ.

For a specification $\exists YF(X,Y)$, the number of Skolem functions itself
can be as large as $2^{n\cdot 2^{m}}$, and the values of $n$ and $m$ are quite
large in many practical cases. Beyond being a theoretical possibility, the
count of Skolem functions is often quite big, and such values are sometimes
difficult to manipulate and store as 64-bit values. Therefore, we are
interested in the logarithm of the counts only, and define the problem of
approximate Skolem function counting as following:

#### Problem Statement.

Given a Boolean specification $F(X,Y)$, tolerance parameter $\varepsilon$,
confidence parameter $\delta$, let $\ell=\log(|\mathsf{Skolem}(F,Y)|)$, the
task of approximate Skolem function count is to give an estimate
$\mathsf{Est}$, such that
$\Pr\left[{(1-\varepsilon){\ell}}\leq\mathsf{Est}\leq(1+\varepsilon)\ell\right]\geq
1-\delta$.

In practical scenarios, the input _specification_ is often given as quantified
Boolean formulas (QBF). The output of synthesis problem is a function, which
is expressed as a Boolean circuit. In our setting, even if two functions have
different circuits, if they have identical input-output behavior, we consider
them to be the same function. For example, let $f_{1}(x)=x$ and
$f_{2}=\neg(\neg x)$. We’ll consider $f_{1}$ and $f_{2}$ to be the same
function.

#### Illustrative Example.

Let’s examine a formula $\exists Y_{0}Y_{1}F(X,Y_{0}Y_{1})$ defined on three
sets of variables $X,Y_{0},Y_{1}$, where each set contains five Boolean
variables and interpreted as five-bit integers. $F$ represents the constraint
for factorization: $X=Y_{0}\times Y_{1},Y_{0}\leq Y_{1},Y_{0}\neq 1$. The
problem of counting Skolem functions of $F$ aims to determine the number of
distinct ways to implement a factorization function for 5-bit input numbers.
There exist multiple $X$’s for which there are multiple factorizations: A
Skolem function $S_{1}$ may factorize $12$ as $4\times 3$ and a function
$S_{2}$ may factorize $12$ as $2\times 6$.

#### Stopping Rule Algorithm.

Let $Z_{1},Z_{2},\dots$ denote independently and identically distributed
(i.i.d.) random variables taking values in the interval $[0,1]$ and with mean
$\mu$. Intuitively, $Z_{t}$ is the outcome of experiment $t$. Then the
Stopping Rule algorithm (Algorithm 1) approximates $\mu$ as stated by Theorem
3.1 (Dagum et al. 1995; Dagum and Luby 1997).

Algorithm 1 Stopping Rule $(\varepsilon,\delta)$

1:$t\leftarrow 0,x\leftarrow 0,s\leftarrow
4\ln(2/\delta)(1+\varepsilon)/\varepsilon^{2}$

2:while $x<s$ do

3: $t\leftarrow t+1$

4: Generate Random Variable $Z_{t}$

5: $x\leftarrow x+Z_{t}$

6:$\mathsf{Est}\leftarrow s/t$

7:return $\mathsf{Est}$

######  Theorem 3.1 (Stopping Rule Theorem).

For all $0<\varepsilon\leq 2,\delta>0$, if the Stopping Rule algorithm returns
$\mathsf{Est}$, then

$\Pr[\mu(1-\varepsilon)\leq\mathsf{Est}\leq\mu(1+\varepsilon)]>(1-\delta)$

#### FPRAS.

A Fully Polynomial Randomized Approximation Scheme (FPRAS) is a randomized
algorithm that, for any fixed $\varepsilon>0$ and any fixed probability
$\delta>0$, produces an answer that is within a factor of $(1+\varepsilon)$ of
the correct answer, and does so with probability at least $(1-\delta)$, in
polynomial time with respect to the size of the input, $1/\varepsilon$, and
$\log(1/\delta)$.

##  4 Algorithm

In this section, we introduce the primary contribution of our paper: the
$\mathsf{SkolemFC}$ algorithm. The algorithm takes in a formula $\exists
YF(X,Y)$ and returns an estimate for $\log(|\mathsf{Skolem}(F,Y)|)$. We first
outline the key technical ideas that inform the design of $\mathsf{SkolemFC}$
and then present the pseudocode for implementing this algorithm.

###  4.1 Core Ideas

Since finding even a single Skolem function is computationally expensive, our
approach is to estimate the count of Skolem functions without enumerating even
a small number of Skolem functions. The key idea is to observe that the number
of Skolem functions can be expressed as a product of the model counts of
formulas. A Skolem function $\Psi\in\mathsf{Skolem}(F,Y)$ is a function from
$2^{X}$ to $2^{Y}$. A useful quantity in the context of counting Skolem
functions is to define, for every assignment $\sigma\in 2^{X}$, the set of
elements in $2^{Y}$ that $\Psi(X)$ can belong to. We refer to this quantity as
$\mathsf{range}(\sigma)$ and formally define it as follows:

######  Definition 4.1.

$\displaystyle\mathsf{range}(\sigma)=\begin{cases}\mathsf{Sol}(F\wedge(X=\sigma))_{\downarrow{Y}}&|\mathsf{Sol}(F\wedge(X=\sigma))|>0\\\
2^{Y}&\text{otherwise}\end{cases}$

######  Lemma 4.2.

$|\mathsf{Skolem}(F,Y)|=\prod\limits_{\sigma\in
2^{X}}|\mathsf{range}(\sigma)|$

###### Proof.

First of all, we observe that

$\displaystyle\forall\sigma\in
2^{X},\forall\pi\in\mathsf{range}(\sigma),\exists\Psi\text{ s.t.
}\Psi(\sigma)=\pi$

The above observation is easy to see for all $\sigma\in 2^{X}$ for which
exists $\pi\in 2^{Y}$ such that $F(\sigma,\pi)=1$. It is worth remarking that
for all $\sigma\in 2^{X}$ for which there is no $\pi$ such that
$F(\sigma,\pi)=1$, there are no restrictions on the output of a Skolem
function $\Psi$ when $X=\sigma$, and consequently, $\Psi(\sigma)$ can take an
arbitrary value from $2^{Y}$. Recall, $\mathsf{Skolem}(F,Y)$ is the set of all
functions from $2^{X}$ to $2^{Y}$, it follows that

$\displaystyle|\mathsf{Skolem}(F,Y)|$ $\displaystyle=\prod\limits_{\sigma\in
2^{X}}|\mathsf{range}(\sigma)|$

∎

Lemma 4.2 allows us to develop a connection between Skolem function counting
and propositional model counting. There is, however, a caveat: the expression
obtained so far requires us to compute propositional model counts for
$|S_{2}|$ formulas, which can be $2^{n}$ in the worst case. To this end, we
focus on estimating $\log|\mathsf{Skolem}(F,Y)|$. To formalize our approach,
we need to introduce the following notation:

######  Definition 4.3.

Let $2^{X}=S_{0}\uplus S_{1}\uplus S_{2}$ where $\uplus$ indicates disjoint
union and the sets $S_{0},S_{1},$ and $S_{2}$ are defined as follows:

$\displaystyle S_{0}$ $\displaystyle:=\\{\sigma\in
2^{X}\mid|\mathsf{Sol}(F\wedge(X=\sigma))|=0\\}$ $\displaystyle S_{1}$
$\displaystyle:=\\{\sigma\in 2^{X}\mid|\mathsf{Sol}(F\wedge(X=\sigma))|=1\\}$
$\displaystyle S_{2}$ $\displaystyle:=\\{\sigma\in
2^{X}\mid|\mathsf{Sol}(F\wedge(X=\sigma))|\geq 2\\}$

######  Proposition 4.4.

$\log|\mathsf{Skolem}(F,Y)|=m\cdot|S_{0}|+\sum\limits_{\sigma\in
S_{2}}\log|\mathsf{Sol}(F\wedge(X=\sigma))|$

###### Proof.

From Lemma 4.2, we have $|\mathsf{Skolem}(F,Y)|=\prod\limits_{\sigma\in
2^{X}}|\mathsf{range}(\sigma)|$. Taking logs on both sides, partitioning
$2^{X}$ into $S_{0},S_{1},S_{2}$, and observing that
$\log|\mathsf{range}(\sigma)|=0$ for $\sigma\in S_{1}$, we get the desired
result. ∎

We’ll use the notation $\mathsf{sk}_{0}$ to denote the factor $m\cdot|S_{0}|$
and $\mathsf{sk}_{1}$ for $\sum\limits_{\sigma\in
S_{2}}\log|\mathsf{Sol}(F\wedge(X=\sigma))$.

Algorithm 2 $\mathsf{SkolemFC}$$(F(X,Y),\varepsilon,\delta)$

1:$\varepsilon_{f}\leftarrow 0.6\varepsilon,\delta_{f}\leftarrow
0.5\delta,s\leftarrow 4\ln(2/\delta)(1+\varepsilon_{f})/{\varepsilon_{f}}^{2}$

2:$\mathsf{Est}_{0}\leftarrow m\times\log(2^{n}-{\mathsf{Count}}(F,X))$

3:$G(X,Y,Y^{\prime}):=F(X,Y)\wedge F(X,Y^{\prime})\wedge(Y\neq Y^{\prime})$

4:$\varepsilon_{s}\leftarrow
0.3\varepsilon,\delta_{c}=\delta/2ms,\varepsilon_{c}\leftarrow 4\sqrt{2}-1$

5:while $x<s$ do

6: $\sigma\leftarrow{\mathsf{AlmostUniformSample}}(G,X,\varepsilon_{s})$

7:
$c\leftarrow\log({\mathsf{ApproxCount}}(F\wedge(X=\sigma),\varepsilon_{c},\delta_{c}))/m$

8: $x\leftarrow x+c$

9: $t\leftarrow t+1$

10:$g\leftarrow\mathsf{Count}(G,X)$

11:$\mathsf{Est}_{1}\leftarrow s/{{t}}\times m\times g$

12:if $(g\log(1+\varepsilon_{c})>0.1\mathsf{Est}_{1})$ then return $\bot$

13:$\mathsf{Est}\leftarrow\mathsf{Est_{0}}+\mathsf{Est_{1}}$

14:return $\mathsf{Est}$

###  4.2 Algorithm Description

The pseudocode for $\mathsf{SkolemFC}$ is delineated in Algorithm 2. It
accepts a formula $\exists YF(X,Y)$, a tolerance level $\varepsilon$, and a
confidence parameter $\delta$. The algorithm then provides an approximation of
$\log|\mathsf{Skolem}(F,Y)|$. Following Proposition 4.4, $\mathsf{SkolemFC}$
initially calculates $\mathsf{Est}_{0}$, the value for $m\cdot|S_{0}|$ at line
2. Following this, it determines an $\mathsf{Est}_{1}$, for $\mathsf{sk}_{1}$
within lines 5 to 11. To begin, $\mathsf{SkolemFC}$ almost-uniformly samples
$\sigma$ from $S_{2}$ at random in line 6, utilizing an almost-uniform
sampler. Subsequently, $\mathsf{SkolemFC}$ approximates
$|\mathsf{Sol}(F\wedge(X=\sigma))|$ through an approximate model counter at
line 7. The estimate $\mathsf{Est}_{1}$ is computed by taking the product of
the mean of $c$’s and $|S_{2}|$. In order to sample $\sigma\in S_{2}$,
$\mathsf{SkolemFC}$ constructs the formula $G$ whose solutions, when projected
to $X$ represent all the assignments $\sigma\in S_{2}$ (line 3). Finally,
$\mathsf{SkolemFC}$ returns the estimate as a summation of the estimates of
$\mathsf{Est}_{0}$ and $\mathsf{Est}_{1}$.

The main loop of $\mathsf{SkolemFC}$ (from lines 5 to 9) is based on the
Stopping Rule algorithm presented in Section 2. The Stopping Rule algorithm is
utilized to approximate the mean of a collection of i.i.d. random variables
that fall within the range $[0,1]$. The method repeatedly adds the outcomes of
these variables until the cumulative value reaches a set threshold $s$. This
threshold value is influenced by the input parameters $\varepsilon$ and
$\delta$. The result yielded by the algorithm is represented as $s/t$, where
$t$ denotes the number of random variables aggregated to achieve the threshold
$s$. In the context of $\mathsf{SkolemFC}$, this random variable is defined as
$\log({\mathsf{ApproxCount}}(F\land(X=\sigma),\varepsilon_{c},\delta_{c}))/m$.
Line 12 asserts that the error introduced by the approximate model counting
oracle is within some specific bound.

#### Oracle Access.

We assume access to exact and approximate model counters, which we use as an
oracle. The notation $\mathsf{Count}$$(F,P)$ denotes an invocation of the
model counting oracle for a Boolean formula $F$ and projection set $P$.
Similarly, $\mathsf{ApproxCount}$$(F,P,\varepsilon,\delta)$ represents an
invocation of the approximate model counting oracle on Boolean formula $F$
with a projection set $P$, tolerance parameter $\varepsilon$, and confidence
parameter $\delta$. ${\mathsf{AlmostUniformSample}}(F,S,\varepsilon)$ denotes
an invocation of the almost uniform sampler on a formula $F$, with projection
set $S$ and tolerance parameter $\varepsilon$. The particular choice of values
of $\varepsilon_{s}$, $\varepsilon_{c}$, $\delta_{c}$ used in the counting and
sampling oracle aids us in proving theoretical guarantees for
$\mathsf{SkolemFC}$ in Appendix A.

###  4.3 Illustrative Example

We will now examine the specification of factorization as outlined in Section
3, and investigate how $\mathsf{SkolemFC}$ estimates the count of Skolem
functions meeting that specification.

  1. 1.

$\mathsf{Sol}(F)_{\downarrow{X}}$ represents non-prime numbers less than 32,
therefore $|\mathsf{Sol}(F)_{\downarrow{X}}|=20$. Now,
${\mathsf{Est}_{0}}=10\times(32-20)=120$ at line 2.

  2. 2.

Now in line 3, $\mathsf{SkolemFC}$ constructs the function $G$, where
$\mathsf{Sol}(G)_{\downarrow{X}}=\\{12,16,18,20,24,28,30\\},|\mathsf{Sol}(G)_{\downarrow{X}}|=7$.

  3. 3.

In line 6, it samples $\sigma$ from $\mathsf{Sol}(G)_{\downarrow{X}}$. Let’s
consider $\sigma=30$. Then $\mathsf{Sol}(F\wedge(X=\sigma))_{\downarrow
Y_{0},Y_{1}}=\\{(2,15),(3,10),(5,6)\\}.$ Therefore, $c=\log(3)$ in line 7.

  4. 4.

Suppose in the next iteration it samples $\sigma=16.$ Then
$\mathsf{Sol}(F\wedge(X=\sigma))=\\{(2,8),(4,4)\\}.$ Therefore, $c=\log(2)$ in
line 7.

  5. 5.

Now suppose that the termination condition of line 5 is reached. At this
point, the estimate $\mathsf{Est}_{1}$ returned from line 11 will be
$\approx\frac{(\log(3)+\log(2))}{2}\times 7\approx 6.$

  6. 6.

Finally, $\mathsf{Est}$ will get the value $\mathsf{Est}_{0}$ \+
$\mathsf{Est}_{1}$ = 126.

Note that the approach is in stark contrast to the state-of-the-art counting
techniques in the context of propositional models, which either construct a
compact representation of the entire solution space or rely on the enumeration
of a small number of models.

###  4.4 Analysis of $\mathsf{SkolemFC}$

Let $F(X,Y)$ be a propositional CNF formula over variables $X$ and $Y$. In the
section we’ll show that $\mathsf{SkolemFC}$ works as an approximate counter
for the number of Skolem functions.

We create a formula $G(X,Y,Y^{\prime})=F(X,Y)\wedge
F(X,Y^{\prime})\wedge(Y\neq Y^{\prime})$ from $F(X,Y)$, where $Y^{\prime}$ is
a fresh set of variables and $m=|Y^{\prime}|$. We show that, if we pick a
solution from $G(X,Y,Y^{\prime})=F(X,Y)\wedge F(X,Y^{\prime})\wedge(Y\neq
Y^{\prime})$, then the assignment to $X$ in that solution to $G$ will have at
least two solutions in $F(X,Y)$.

######  Lemma 4.5.

$\mathsf{Sol}(G)_{\downarrow{X}}=\left\\{\sigma\mid\sigma\in
2^{X}\wedge|\mathsf{Sol}(F\wedge(X=\sigma))|\geq 2\right\\}$

###### Proof.

We can write the statement alternatively as,

$\sigma\in\mathsf{Sol}(G,X)\iff|\mathsf{Sol}(F\wedge(X=\sigma))|\geq 2$

$(\implies)$ For every element $\sigma\in\mathsf{Sol}(G)$, we write $\sigma$
as $\langle\sigma_{\downarrow X},\sigma_{\downarrow Y},\sigma_{\downarrow
Y^{\prime}}\rangle$. Now according to the definition of $G$, both
$\langle\sigma_{\downarrow X},\sigma_{\downarrow Y}\rangle$ and
$\langle\sigma_{\downarrow X},\sigma_{\downarrow Y^{\prime}}\rangle$ satisfy
$F$. Moreover, $\sigma_{\downarrow Y}$ and $\sigma_{\downarrow Y^{\prime}}$
are not equal. Therefore, $|\mathsf{Sol}(F\wedge(X=\sigma))|\geq 2$.

$(\impliedby)$ If $|\mathsf{Sol}(F\wedge(X=\sigma))|\geq 2$, then $F(X,Y)$ has
solutions of the form $\langle\sigma,\gamma_{1}\rangle$ and
$\langle\sigma,\gamma_{2}\rangle$, where $\gamma_{1}\neq\gamma_{2}$. Now
$\langle\sigma\gamma_{1}\gamma_{2}\rangle$ satisfies $G$. ∎

######  Theorem 4.6.

Let an invocation of the algorithm $\mathsf{SkolemFC}$ return $\mathsf{Est}$,
and $\ell=\log(|\mathsf{Skolem}(F,Y)|)$. Then

$\displaystyle\Pr\left[{(1-\varepsilon){\ell}}\leq\mathsf{Est}\leq(1+\varepsilon)\ell\right]\geq
1-\delta$

###### Proof.

Refer to Appendix A. ∎

######  Theorem 4.7.

$\mathsf{SkolemFC}$ invokes an approximate model counting oracle and an almost
uniform sampling oracle
$\mathcal{O}\left(4m\ln\frac{2}{\delta}\left(1+\varepsilon\right)/\varepsilon^{2}\right)$
times, and makes two calls to the exact model counting oracle.

###### Proof.

The formula $G$ in 3 of $\mathsf{SkolemFC}$ can be constructed with a time
complexity that is a polynomial in $|F|$. As the minimum value for $c$ in line
7 is 1, the for loop, located between lines 5 and 9, is executed a maximum of
${t}=\left(4m\ln(2/\delta)(1+\varepsilon_{f})/\varepsilon_{f}^{2}\right)$
times. During each iteration, the algorithm makes one call to an approximate
counting oracle and an almost uniform sampling oracle, resulting in a total of
${t}$ calls to these oracles. Now $\varepsilon_{f}=0.6\varepsilon$, the total
number of approximate model counting oracle calls made and an almost uniform
sampling oracle is
$\mathcal{O}\left(4m\ln(2/\delta)(1+\varepsilon)/\varepsilon^{2}\right)$. ∎

##  5 Experiments

We conducted a thorough evaluation of the performance and accuracy of results
of the $\mathsf{SkolemFC}$ algorithm by implementing a functional
prototype.111Source code:
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}https://github.com/meelgroup/skolemfc/}$
Our prototype implementation integrates Python and Linux shell scripting. The
following experimental setup was used to evaluate the performance and quality
of results of the $\mathsf{SkolemFC}$ algorithm222All benchmarks and
experimental data are available at
$\mathtt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}https://doi.org/10.5281/zenodo.10404174}$.

#### Baseline.

A possible option to get the exact count the Skolem functions is using Lemma
4.2. We describe the complete algorithm in Algorithm 3 and implemented that to
compare with $\mathsf{SkolemFC}$. In the implementation, we relied on the
latest version of $\mathsf{Ganak}$ (Sharma et al. 2019) to get the necessary
exact model counts. We use a modified version of the SAT solver
$\mathsf{CryptoMiniSat}$ (Soos, Nohl, and Castelluccia 2009) as
$\mathsf{AllSAT}$ solver to get all the solution of a given formula, projected
on $X$ variables. We call this implementation $\mathsf{Baseline}$ in the
following part of the paper.

Algorithm 3 $\mathsf{Baseline}$$(F(X,Y))$

1:$\mathsf{Est}_{0}\leftarrow
m\times\log(2^{n}-{\mathsf{Count}}(F,X)),x\leftarrow 0$

2:$G(X,Y,Y^{\prime}):=F(X,Y)\wedge F(X,Y^{\prime})\wedge(Y\neq Y^{\prime})$

3:$\mathsf{SolG}\leftarrow\mathsf{AllSAT}(G,X)$

4:for each $\sigma\in\mathsf{SolG}$ do

5: $c\leftarrow\log({\mathsf{Count}}(F\wedge(X=\sigma)))$

6: $x\leftarrow x+c$

7:$\mathsf{Est}\leftarrow\mathsf{Est_{0}}+x$

8:return $\mathsf{Est}$

#### Environment.

All experiments were carried out on a high-performance computer cluster, where
each node consists of AMD EPYC 7713 CPUs running with 2x64 real cores. All
tools were run in a single-threaded mode on a single core with a timeout of 10
hrs, i.e., 36000 seconds. A memory limit was set to 16 GB per core.

#### Parameters for Oracles and Implementation.

In the implementation, we utilized different state-of-the-art tools as
counting and sampling oracles, including $\mathsf{UniSamp}$ (Delannoy and Meel
2022) as an almost uniform sampling oracle, $\mathsf{GPMC}$ (Suzuki,
Hashimoto, and Sakai 2017) for an exact (projected) counting oracle, and the
latest version of $\mathsf{ApproxMC}$ (Yang and Meel 2023) as an approximate
counting oracle. $\mathsf{SkolemFC}$ was tested with $\varepsilon=0.8$ and
$\delta=0.8$. That gave the following values to error and tolerance parameters
for model counting and sampling oracles. The almost uniform sampling oracle
$\mathsf{UniSamp}$ is run with $\varepsilon_{s}=0.24$. The approximate model
counting oracle $\mathsf{ApproxMC}$ was run with $\varepsilon_{c}=4\sqrt{2}-1$
and $\delta_{c}=\frac{0.4}{m*s}$, where $s$ and $m$ come from the algorithm,
based on the instance. We carefully select error and tolerance values
$\varepsilon_{s},\varepsilon_{c},\delta_{c}$ for counting and sampling oracles
to ensure the validity of final bounds for $\mathsf{SkolemFC}$ while also
aiming for optimal performance of the counter based on these choices. The
relationship between these values and the validity of bound of
$\mathsf{SkolemFC}$ is illustrated in the proof of Theorem 4.6.

In our experiments, we sought to evaluate the run-time performance and
approximation accuracy of $\mathsf{SkolemFC}$. Specifically, the following
research questions guided our investigation:

  1. RQ1.

How does $\mathsf{SkolemFC}$ scale in terms of solving instances and the time
taken in our benchmark set?

  2. RQ2.

What is the precision of the $\mathsf{SkolemFC}$ approximation, and does it
outperform its theoretical accuracy guarantees in practical scenarios?

#### Benchmarks.

To evaluate the performance of $\mathsf{SkolemFC}$, we chose two sets
benchmark suite.

  1. 1.

_Efficiency benchmarks._ 609 instances from recent works on Boolean function
synthesis (Golia, Roy, and Meel 2020; Akshay et al. 2017), which includes
different sources: the Prenex-2QBF track of QBFEval-17 (qbf 2017), QBFEval-18
(qbf 2018), disjunctive (Akshay et al. 2017), arithmetic (Tabajara and Vardi
2017) and factorization (Akshay et al. 2017).

  2. 2.

_Correctness Benchmarks._ The benchmarks described in the paragraph above are
too hard for the baseline algorithm to solve. As Section 5.1 reveals, the
number of instances solved by the baseline is just eight out of the 609
instances. Therefore, to check the correctness of $\mathsf{SkolemFC}$ (RQ2),
we used a set of 158 benchmarks from SyGuS instances (Golia, Roy, and Meel
2021). These benchmarks have very few input variables $(m\leq 8)$, and takes
seconds for $\mathsf{SkolemFC}$ to solve.

#### Summary of Results.

$\mathsf{SkolemFC}$ achieves a huge improvement over $\mathsf{Baseline}$ by
resolving 379 instances in a benchmark set consisting of 609, while
$\mathsf{Baseline}$ only solved 8. The accuracy of the approximate count is
also noteworthy, with an average error shown by a count of $\mathsf{SkolemFC}$
is only 21%.

###  5.1 Performance of $\mathsf{SkolemFC}$

We evaluate the performance of $\mathsf{SkolemFC}$ based on two metrics: the
number of instances solved and the time taken to solve the instances.

Algorithm | # Instances solved
---|---
$\mathsf{Baseline}$ | 8
$\mathsf{SkolemFC}$ | 379
Table 1: Instances solved by $\mathsf{SkolemFC}$ and $\mathsf{Baseline}$ out
of 64 benchmarks.  Figure 1: Runtime performance between $\mathsf{SkolemFC}$
and $\mathsf{Baseline}$.

#### Instances Solved.

In Table 1, we compare the number of benchmarks that can be solved by
$\mathsf{Baseline}$ and $\mathsf{SkolemFC}$. First, it is evident that the
$\mathsf{Baseline}$ only solved 8 out of the 609 benchmarks in the test suite,
indicating its lack of scalability for practical use cases. Conversely,
$\mathsf{SkolemFC}$ solved 379 instances, demonstrating a substantial
improvement compared to $\mathsf{Baseline}$.

#### Solving Time Comparison.

A performance evaluation of $\mathsf{Baseline}$ and $\mathsf{SkolemFC}$ is
depicted in Figure 1, which is a cactus plot comparing the solving time. The
$x$-axis represents the number of instances, while the $y$-axis shows the time
taken. A point $(i,j)$ in the plot represents that a solver solved $j$
benchmarks out of the 609 benchmarks in the test suite in less than or equal
to $j$ seconds. The curves for $\mathsf{Baseline}$ and $\mathsf{SkolemFC}$
indicate that for a few instances, $\mathsf{Baseline}$ was able to give a
quick answer, while in the long run, $\mathsf{SkolemFC}$ could solve many more
instances given any fixed timeout.

#### Counter Call Comparison.

We analyze the algorithms’ complexity in terms of counter calls, comparing
$\mathsf{Baseline}$ and $\mathsf{SkolemFC}$ across benchmarks in Figure 2. The
$x$ axis represents benchmarks, and the $y$ axis shows required counter calls,
sorted by the increasing order of calls needed by $\mathsf{Baseline}$. A red
or green point $(i,j)$ signifies that $\mathsf{Baseline}$ or
$\mathsf{SkolemFC}$, respectively, requires $j$ counting oracle calls for the
$i^{th}$ instance. $\mathsf{Baseline}$ requires up to a staggering $10^{230}$
counter calls for some instances, emphasizing the need for a scalable
algorithm like $\mathsf{SkolemFC}$, which incurs significantly fewer counter
calls.

Figure 2: Counter calls needed by $\mathsf{SkolemFC}$ and $\mathsf{Baseline}$
to solve the benchmarks.

We analyze the scalability of $\mathsf{SkolemFC}$ by examining the correlation
between average time per counter call and total counter calls, depicted in
Figure 3. The point $(i,j)$ means that if $\mathsf{SkolemFC}$ needs $i$
counter calls, the average time per call is $j$ seconds. The figure showcases
diverse scenarios: some with fewer iterations and longer durations per call,
others with high counts and minimal time per call.

Figure 3: Relation between number of iterations needed by $\mathsf{SkolemFC}$
and average time taken in each counter call.

###  5.2 Quality of Approximation

In the experiments, 158 accuracy benchmarks were measured using
$\mathsf{Baseline}$, enabling comparison between $\mathsf{Baseline}$ and
$\mathsf{SkolemFC}$ results, shown in Figure 4. The counts’ close alignment
and error reduction below theoretical guarantees were observed. We quantify
the $\mathsf{SkolemFC}$ performance with error $e=\frac{|b-s|}{b}$, where $b$
is the count from $\mathsf{Baseline}$ and $s$ from $\mathsf{SkolemFC}$.
Analysis of all 158 cases found the average $e$ to be $0.21$, geometric mean
$0.19$, and maximum $0.496$, contrasting sharply with a theoretical guarantee
of $0.8$. This signifies $\mathsf{SkolemFC}$ substantially outperforms its
theoretical bounds. Our findings underline $\mathsf{SkolemFC}$’s accuracy and
potential as a dependable tool for various applications.

Figure 4: Count estimate returned by $\mathsf{SkolemFC}$, vs. the theoretical
bounds.

##  6 Conclusion

In conclusion, this paper presents the first scalable approximate Skolem
function counter, $\mathsf{SkolemFC}$, which has been successfully tested on
practical benchmarks and showed impressive performance. Our proposed method
employs probabilistic techniques to provide theoretical guarantees for its
results. The implementation leverages the progress made in the last two
decades in the fields of constrained counting and sampling, and the practical
results exceeded the theoretical guarantees. These findings raise several
important open questions that warrant further investigation. One such area of
potential extension is the application of the algorithm to other types of
functions, such as counting uninterpreted functions in SMT with a more general
syntax. This extension would enable the algorithm to handle a broader range of
applications and provide even more accurate results. In summary, this research
contributes significantly to the field of Skolem function counting and
provides a foundation for further studies.

## Acknowledgements

We are thankful to Tim van Bremen and Priyanka Golia for providing detailed
feedback on the early drafts of the paper and grateful to the anonymous
reviewers for their constructive comments to improve this paper. This work was
supported in part by National Research Foundation Singapore under its NRF
Fellowship Programme [NRF-NRFFAI1-2019-0004], Ministry of Education Singapore
Tier 2 Grant [MOE-T2EP20121-0011], Ministry of Education Singapore Tier 1
Grant [R-252-000-B59-114], and NSF awards IIS-1908287, IIS-1939677, and
IIS-1942336. Part of the work was done during Arijit Shaw’s internship at the
National University of Singapore. The computational work for this article was
performed on resources of the National Supercomputing Centre, Singapore
(https://www.nscc.sg).

## References

  * qbf (2017) 2017\.  QBF solver evaluation portal 2017.
  * qbf (2018) 2018\.  QBF solver evaluation portal 2018.
  * Akshay et al. (2019) Akshay, S.; Arora, J.; Chakraborty, S.; Krishna, S.; Raghunathan, D.; and Shah, S. 2019.  Knowledge Compilation for Boolean Functional Synthesis.  In _Proc. of FMCAD_.
  * Akshay et al. (2018) Akshay, S.; Chakraborty, S.; Goel, S.; Kulal, S.; and Shah, S. 2018.  What’s hard about Boolean Functional Synthesis?  In _Proc. of CAV_.
  * Akshay et al. (2017) Akshay, S.; Chakraborty, S.; John, A. K.; and Shah, S. 2017.  Towards parallel Boolean functional synthesis.  In _Proc. of TACAS_ , 337–353. Springer.
  * Albarghouthi, Dillig, and Gurfinkel (2016) Albarghouthi, A.; Dillig, I.; and Gurfinkel, A. 2016.  Maximal specification synthesis.  _ACM SIGPLAN Notices_.
  * Ansótegui, Bonet, and Levy (2013) Ansótegui, C.; Bonet, M. L.; and Levy, J. 2013.  SAT-based MaxSAT algorithms.  _Artificial Intelligence_ , 196: 77–105.
  * Balabanov and Jiang (2011) Balabanov, V.; and Jiang, J.-H. R. 2011.  Resolution proofs and Skolem functions in QBF evaluation and applications.  In _Proc. of CAV_.
  * Baudry and Monperrus (2015) Baudry, B.; and Monperrus, M. 2015.  The multiple facets of software diversity: Recent developments in year 2000 and beyond.  _ACM Computing Surveys (CSUR)_ , 48(1): 1–26.
  * Becker et al. (2012) Becker, B.; Ehlers, R.; Lewis, M.; and Marin, P. 2012.  ALLQBF solving by computational learning.  In _International Symposium on Automated Technology for Verification and Analysis_ , 370–384. Springer.
  * Chakraborty et al. (2018) Chakraborty, S.; Fried, D.; Tabajara, L. M.; and Vardi, M. Y. 2018.  Functional synthesis via input-output separation.  In _Proc. of FMCAD_.
  * Chakraborty et al. (2016) Chakraborty, S.; Meel, K.; Mistry, R.; and Vardi, M. 2016.  Approximate probabilistic inference via word-level counting.  In _Proc. of AAAI_ , volume 30.
  * Chakraborty, Meel, and Vardi (2013) Chakraborty, S.; Meel, K. S.; and Vardi, M. Y. 2013.  A scalable approximate model counter.  In _Proc. of CP_.
  * Chakraborty, Meel, and Vardi (2014) Chakraborty, S.; Meel, K. S.; and Vardi, M. Y. 2014.  Balancing Scalability and Uniformity in SAT-Witness Generator.  In _Proc. of DAC_ , 60:1–60:6.
  * Chakraborty, Meel, and Vardi (2016) Chakraborty, S.; Meel, K. S.; and Vardi, M. Y. 2016.  Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls.  In _Proc. of IJCAI_ , 3569–3576.
  * Chakraborty, Meel, and Vardi (2021) Chakraborty, S.; Meel, K. S.; and Vardi, M. Y. 2021.  Approximate model counting.  In _Handbook of Satisfiability_.
  * Chistikov, Dimitrova, and Majumdar (2015) Chistikov, D.; Dimitrova, R.; and Majumdar, R. 2015.  Approximate counting in SMT and value estimation for probabilistic programs.  In _Proc. of TACAS_ , 320–334. Springer.
  * Dagum et al. (1995) Dagum, P.; Karp, R.; Luby, M.; and Ross, S. 1995.  An optimal algorithm for Monte Carlo estimation.  In _Proceedings of IEEE 36th Annual Foundations of Computer Science_.
  * Dagum and Luby (1997) Dagum, P.; and Luby, M. 1997.  An optimal approximation algorithm for Bayesian inference.  _Artificial Intelligence_.
  * Delannoy and Meel (2022) Delannoy, R.; and Meel, K. S. 2022.  On Almost-Uniform Generation of SAT Solutions: The power of 3-wise independent hashing.  In _Proc. of LICS_.
  * Dudek, Phan, and Vardi (2020) Dudek, J. M.; Phan, V. H.; and Vardi, M. Y. 2020.  ADDMC: Weighted model counting with algebraic decision diagrams.  _Proc. of AAAI_ , 1468–1476.
  * Durand et al. (2021) Durand, A.; Haak, A.; Kontinen, J.; and Vollmer, H. 2021.  Descriptive complexity of #P functions: A new perspective.  _Journal of Computer and System Sciences_ , 116: 40–54.
  * Froleyks et al. (2021) Froleyks, N.; Heule, M.; Iser, M.; Järvisalo, M.; and Suda, M. 2021.  SAT competition 2020.  _Artificial Intelligence_.
  * Golia, Roy, and Meel (2020) Golia, P.; Roy, S.; and Meel, K. S. 2020.  Manthan: A data-driven approach for Boolean function synthesis.  In _Proc. of CAV_ , 611–633. Springer.
  * Golia, Roy, and Meel (2021) Golia, P.; Roy, S.; and Meel, K. S. 2021.  Program Synthesis as Dependency Quantified Formula Modulo Theory.  In _Proc. of IJCAI_.
  * Golia et al. (2021) Golia, P.; Slivovsky, F.; Roy, S.; and Meel, K. S. 2021.  Engineering an efficient boolean functional synthesis engine.  In _Proc. of ICCAD_ , 1–9. IEEE.
  * Gomes, Sabharwal, and Selman (2021) Gomes, C. P.; Sabharwal, A.; and Selman, B. 2021.  Model counting.  In _Handbook of satisfiability_ , 993–1014. IOS press.
  * Haak and Vollmer (2019) Haak, A.; and Vollmer, H. 2019.  A model-theoretic characterization of constant-depth arithmetic circuits.  _Annals of Pure and Applied Logic_ , 170(9): 1008–1029.
  * Jiang (2009) Jiang, J.-H. R. 2009.  Quantifier elimination via functional composition.  In _Proc. of CAV_.
  * Jiang, Lin, and Hung (2009) Jiang, J. R.; Lin, H.; and Hung, W. 2009.  Interpolating functions from large Boolean relations.  In _Proc. of ICCAD_.
  * John et al. (2015) John, A. K.; Shah, S.; Chakraborty, S.; Trivedi, A.; and Akshay, S. 2015.  Skolem functions for factored formulas.  In _Proc. of FMCAD_.
  * Kroening and Strichman (2016) Kroening, D.; and Strichman, O. 2016.  _Decision procedures_.  Springer.
  * Li and Manya (2021) Li, C. M.; and Manya, F. 2021.  MaxSAT, hard and soft constraints.  In _Handbook of satisfiability_.
  * Prabhu et al. (2021) Prabhu, S.; Fedyukovich, G.; Madhukar, K.; and D’Souza, D. 2021.  Specification synthesis with constrained Horn clauses.  In _Proc. of PLDI_ , 1203–1217.
  * Rabe (2019) Rabe, M. N. 2019.  Incremental Determinization for Quantifier Elimination and Functional Synthesis.  In _Proc. of CAV_.
  * Rabe and Seshia (2016) Rabe, M. N.; and Seshia, S. A. 2016.  Incremental Determinization.  In _Proc. of SAT_.
  * Rabe et al. (2018) Rabe, M. N.; Tentrup, L.; Rasmussen, C.; and Seshia, S. A. 2018.  Understanding and extending incremental determinization for 2QBF.  In _Proc. of CAV_.
  * Sharma et al. (2019) Sharma, S.; Roy, S.; Soos, M.; and Meel, K. S. 2019.  GANAK: A Scalable Probabilistic Exact Model Counter.  In _Proc. of IJCAI_ , volume 19, 1169–1176.
  * Shukla et al. (2022) Shukla, A.; Möhle, S.; Kauers, M.; and Seidl, M. 2022.  Outercount: A first-level solution-counter for quantified boolean formulas.  In _International Conference on Intelligent Computer Mathematics_ , 272–284. Springer.
  * Soos, Nohl, and Castelluccia (2009) Soos, M.; Nohl, K.; and Castelluccia, C. 2009.  Extending SAT Solvers to Cryptographic Problems.  In _Proc. of SAT_ , 244. Springer.
  * Suzuki, Hashimoto, and Sakai (2017) Suzuki, R.; Hashimoto, K.; and Sakai, M. 2017.  Improvement of projected model-counting solver with component decomposition using SAT solving in components.  Technical report, JSAI Technical Report, SIG-FPAI-506-07.
  * Tabajara and Vardi (2017) Tabajara, L. M.; and Vardi, M. Y. 2017.  Factored Boolean functional synthesis.  In _Proc. of FMCAD_ , 124–131. IEEE.
  * Thurley (2006) Thurley, M. 2006.  sharpSAT–counting models with advanced component caching and implicit BCP.  In _Proc. of SAT_.
  * Yang and Meel (2023) Yang, J.; and Meel, K. S. 2023.  Rounding Meets Approximate Model Counting.  In _Proc. of CAV_.

##  Appendix A Proof of Theorem 4.6

###### Proof.

There are three sources of error in the approximation of the count. In the
following table we list those. We’ll use the following shorthand notation
$\mathsf{LC}(\sigma)$ for $\log(|\mathsf{Sol}(F\wedge X=\sigma)|)$.

Reason of Error | Estimated Amount
---|---
Approximation by $\mathsf{SkolemFC}$ $(E_{F})$ | $\varepsilon_{f}\displaystyle\sum_{\sigma\in S_{2}}\mathsf{LC}(\sigma)$
Non-uniformity in Sampling $(E_{S})$ | $\varepsilon_{s}\displaystyle\sum_{\sigma\in S_{2}}\mathsf{LC}(\sigma)$
Approximation by $\mathsf{ApproxCount}$$(E_{M})$ | $|S_{2}|\log(1+\varepsilon_{c})$

In this section, we will establish the significance of the bounds on
individual errors, culminating in a demonstration of how these errors combine
to yield the error bound for $\mathsf{SkolemFC}$.
(1) Bounding the error from $\mathsf{SkolemFC}$.
For a given formula $\exists YF(X,Y)$, we partition $2^{X}$, the assignment
space of $X$, into three subsets, $S_{0},S_{1},S_{2}$ as discussed in Section
4.1. In line 5 of Algorithm 2, we pick an assignment to $X$ almost uniformly
at random from $\mathsf{Sol}(G)_{\downarrow{X}}$. Let $\sigma_{i}$ be the
random assignment picked at $i^{th}$ iteration of the for loop. For each of
the random event of picking an assignment $\sigma_{i}$, we define a random
variable $W_{i}$ such that, $W_{i}$ becomes a function of $\sigma_{i}$ in the
following way:

$W_{i}=\displaystyle\frac{\log(|\mathsf{Sol}(F\wedge(X=\sigma_{i}))|)}{m}$

Therefore, we have ${t}$ random variables $W_{1},W_{2},\dots W_{{t}}$ on the
sample space of $S_{2}$. Now as $\sigma_{i}$ is picked from
$\mathsf{Sol}(G)_{\downarrow{X}}$ at line 3 of $\mathsf{SkolemFC}$, from Lemma
4.5 we know, $2\leq|\mathsf{Sol}(F\wedge(X=\sigma_{i}))|$. Therefore the
following holds,

$\displaystyle\forall i,2\leq|\mathsf{Sol}(F\wedge(X=\sigma_{i}))|\leq 2^{m}$

Hence, from the definition of $W_{i}$:

$\displaystyle\forall i,\frac{1}{m}\leq W_{i}\leq 1$

Now assume that the model counting oracle of line 7 returns an exact model
count instead of an approximate model count; and the value retured at line 11
is $\mathsf{EEst}$ instead of $\mathsf{Est}_{1}$. Now, due to approximation by
$\mathsf{SkolemFC}$, according to Theorem 3.1 (stopping rule theorem),

$\Pr\left[\left|\frac{\mathsf{EEst}}{m|S_{2}|}-\mu\right|\leq\varepsilon_{f}\mu\right]\geq
1-\delta_{f}$ (1)

(2) Bounding the error from sampling oracle.

Let $p_{j}$ be the probability an assignment $\sigma_{j}\in S_{2}$ appears.
Then,

$\mu=E[W_{i}]=\sum_{\sigma_{j}\in
S_{2}}p_{j}\frac{\mathsf{LC}(\sigma_{j})}{m}$

Now from the guarantee provided by the almost oracle, we know

$\displaystyle\frac{1}{(1+\varepsilon_{s})|S_{2}|}\leq
p_{j}\leq\frac{(1+\varepsilon_{s})}{|S_{2}|}$

Therefore,

$\displaystyle\frac{\displaystyle\sum_{\sigma\in
S_{2}}\mathsf{LC}(\sigma)}{m|S_{2}|(1+\varepsilon_{s})}\leq\mu\leq\frac{(1+\varepsilon_{s})\displaystyle\sum_{\sigma\in
S_{2}}\mathsf{LC}(\sigma)}{m|S_{2}|}$
$\left|m|S_{2}|\mu-\displaystyle\sum_{\sigma\in
S_{2}}\mathsf{LC}(\sigma)\right|\leq E_{S}$ (2)

(3) Bounding the error from counting oracle.
We’ll use the following shorthand notation $\mathsf{LA}(\sigma)$ for
$\log(\mathsf{ApproxCount}(F\wedge X=\sigma,\varepsilon_{c},\delta_{c}))$.
From properties of $\mathsf{ApproxCount}$ oracle, for arbitrary $\sigma$,

$\Pr[|\mathsf{LC}(\sigma)-\mathsf{LA}(\sigma)|\leq\log(1+\varepsilon_{c})]\geq
1-\delta_{c}$

Let $S_{s}\subseteq S_{2}$ be the set of $t$ samples picked up at line 6. ($t$
is the number of iterations taken by the algorithm, as in line 9):

$\Pr\left[\left|\displaystyle\sum_{\sigma\in
S_{s}}\mathsf{LA}(\sigma)-\displaystyle\sum_{\sigma\in
S_{s}}\mathsf{LC}(\sigma)\right|\leq t\log(1+\varepsilon_{c})\right]\geq
1-t\delta_{c}$ (3)

Now $\mathsf{EEst}=\frac{|S_{2}|}{t}\displaystyle\sum_{\sigma\in
S_{s}}\mathsf{LC}(\sigma)$ and
$\mathsf{Est}_{1}=\frac{|S_{2}|}{t}\displaystyle\sum_{\sigma\in
S_{s}}\mathsf{LA}(\sigma)$. Therefore,

$\Pr\left[\left|\mathsf{EEst}-\mathsf{Est}_{1}\right|\leq E_{M}\right]\geq
1-t\delta_{c}$ (4)

(4) Summing-up all the errors.
Combining Equation 1 and (2)

$\Pr\left[\left|\mathsf{EEst}-\displaystyle\sum_{\sigma\in
S_{2}}\mathsf{LC}(\sigma)\right|\leq E_{S}+E_{F}\right]\geq 1-\delta_{f}$ (5)

Combining Equation 4 and (5), putting $\delta=\delta_{f}+t\delta_{c}$

$\Pr\left[\left|\mathsf{Est}_{1}-\displaystyle\sum_{\sigma\in
S_{2}}\mathsf{LC}(\sigma)\right|\leq E_{S}+E_{M}+E_{F}\right]\geq 1-\delta$
(6)

According to Algorithm 2, $\varepsilon_{s}=0.3\varepsilon$ and
$\varepsilon_{f}=0.6\varepsilon$. Now, line 12 asserts that $E_{M}\leq
0.1\varepsilon\displaystyle\sum_{\sigma\in 2^{X}}\mathsf{LC}(\sigma)$. that
makes $E_{S}+E_{M}+E_{F}\leq\varepsilon\displaystyle\sum_{\sigma\in
S_{2}}\mathsf{LC}(\sigma)$. Moreover,
$\mathsf{Est}=\mathsf{Est}_{1}+\displaystyle\sum_{\sigma\in 2^{X}\backslash
S_{2}}\mathsf{LC}(\sigma)$. Therefore,

$\Pr\left[\left|\mathsf{Est}-\displaystyle\sum_{\sigma\in
2^{X}}\mathsf{LC}(\sigma)\right|\leq\varepsilon\displaystyle\sum_{\sigma\in
2^{X}}\mathsf{LC}(\sigma)\right]\geq 1-\delta$

Or,

$\Pr\left[{(1-\varepsilon){\ell}}\leq\mathsf{Est}\leq(1+\varepsilon)\ell\right]\geq
1-\delta$

where $\ell=\log(|\mathsf{Skolem}(F,Y)|)$. ∎

##  Appendix B Selection of Oracles

In case of $\mathsf{SkolemFC}$, we need access to approximate model counter
and exact projected model counter for which we use $\mathsf{GPMC}$ as it has
been winner of model counting competition projected track for 2021 and 2022.
For our $\mathsf{Baseline}$, we need access to both exact model counter and
exact projected model counter; we used $\mathsf{GPMC}$ for projected model
counter and $\mathsf{Ganak}$ for exact (non-projected) model counter. In
summary, we rely on the best counter for the kind of queries the corresponding
algorithm requires. Note that exact (non-projected) model counter was
necessary for Baseline because we had to perform exponentially (in $m$) many
computations and therefore the errors would compound.

##  Appendix C Some more results

In Table 2, we present the performance of $\mathsf{SkolemFC}$ on selected
benchmarks from our experiments. The table displays the number of input
variables in column $n$ and the number of output variables in column $m$. The
following two columns show the number of counter calls required by
$\mathsf{Baseline}$ and $\mathsf{SkolemFC}$. The final two columns present the
time taken by each algorithm to solve the benchmarks.

|  |  | Counter Calls | Runtime (s)
---|---|---|---|---
Benchmark | $n$ | $m$ | $\mathsf{Baseline}$ | $\mathsf{SkolemFC}$ | $\mathsf{Baseline}$ | $\mathsf{SkolemFC}$
factorization8 | 8 | 87 | 84 | 1197 | 119 | 416
sbug-fp-5 | 17 | 69 | 131072 | 185 | 11680 | 108
sbug-fp-3 | 11 | 41 | 2048 | 175 | 342 | 128
factorization16 | 16 | 374 | 17920 | 4561 | 1788 | 2388
sdyn-partition-fp-1 | 16 | 71 | 65536 | 303 | 3468 | 282
mult9.sat | 19 | 1545 | 262144 | 3289 | TO | 1517
sbug-fp-10 | 32 | 139 | $4.29\text{\times}{10}^{09}$ | 191 | TO | 240
decomposition64 | 64 | 508 | $1.84\text{\times}{10}^{19}$ | 328 | TO | 331
rankfunc38 | 128 | 519 | $3.40\text{\times}{10}^{38}$ | 169 | TO | 431
intermediate64 | 128 | 511 | $3.40\text{\times}{10}^{38}$ | 344 | TO | 813
rankfunc55 | 128 | 1033 | $3.40\text{\times}{10}^{38}$ | 225 | TO | 1057
sdyn-partition-fp-5 | 48 | 501 | $2.81\text{\times}{10}^{14}$ | 508 | TO | 1061
all_bit_differ-29 | 432 | 1204 | $1.11\text{\times}{10}^{130}$ | 248 | TO | 1226
sdlx-fixpoint-1 | 115 | 926 | $4.15\text{\times}{10}^{34}$ | 917 | TO | 1299
intermediate128 | 256 | 1022 | $1.16\text{\times}{10}^{77}$ | 342 | TO | 1393
amba2c7n.sat | 36 | 1345 | $6.87\text{\times}{10}^{10}$ | 1542 | TO | 1455
ceiling64 | 128 | 527 | $3.40\text{\times}{10}^{38}$ | 11218 | TO | 5892
subtraction128 | 256 | 891 | $1.16\text{\times}{10}^{77}$ | 18965 | TO | 15977
usb-phy-fixpoint-5 | 1002 | 8809 | $4.29\text{\times}{10}^{301}$ | 449 | TO | 27467
cache-coh-2-fp-6 | 966 | 10611 | $6.24\text{\times}{10}^{290}$ | 545 | TO | 34871
Table 2: Results on some sample files showing details of the benchmarks and
runtime performance of $\mathsf{SkolemFC}$. Timeout(TO) = 10 hrs.


# On a Relativistic Quark Model Description via the Fractional Nikiforov-
Uvarov Method

M. Abu-Shady  Department of Mathematics and computer science, Faculty of
Science, Menoufia University, Egypt Mohammed K. A. Kaabar  Institute of
Mathematical Sciences, Faculty of Science, Universiti Malaya, Kuala Lumpur
50603, Malaysia

###### Abstract

The Dirac equation plays an essential role in the relativistic quantum
systems, which is reduced to a form similar to Schrodinger equation when a
certain potential’s type is selected as the Cornell potential. By choosing the
generalized fractional derivative, the fractional Nikiforov-Uvarov method is
applied as a good efficient tool. The energy eigenvalues and corresponding
wave functions are obtained in the sense of fractional forms by solving Dirac
equation analytically. The special case is obtained, which is compatible with
the classical model. Solving the fractional Dirac equation will open a new
path to solve and improve results in the classical relativistic quantum
systems.

Keywords: Dirac equation, Fractional Nikiforov-Uvarov method, generalized
fractional derivative.

††preprint:

LABEL:FirstPage1 LABEL:LastPage#1102

##  I Introduction

Fractional-order derivative is basically a natural extension of ordinary
derivatives, which has become a popular research topic in applied sciences
[1-4] and engineering [5, 6]. The non-locality plays a significant role in
fractional derivative models. There are various definitions of fractional
derivatives such as Riemann-Liouville, Caputo, and Hadamard, where each of
them has advantages and disadvantages. Therefore, there is no single
fractional derivative definition that can be applied for all fractional
models. A recently proposed generalization of fractional derivative
$\left[7\right]$, named Abu-Shady–Kaabar fractional derivative (AKFD), obtains
results that are compatible with the classical fractional definitions of
Riemann-Liouville and Caputo. This definition has been given in detail along
with all its related theorems in $\left[7,24\right]$, which can be written as
follows:

$\mathcal{D}^{AKFD}h(t)=\lim_{\Lambda\rightarrow
0}\frac{h(t+\frac{\Gamma(\beta)}{\Gamma(\beta-\alpha+1)}\Lambda
t^{1-\alpha})-h(t)}{\Lambda};\beta>-1,\beta\in R^{+}\vskip 12.0pt plus 4.0pt
minus 4.0pt$ (1)

In Eq. (1), the AKFD operator, denoted by $D^{AKFD}$, is of order $\alpha$.
The field of relativistic quantum mechanics is significant and outstanding.
The relativistic particles’ description with spin (1/2) as in [8] is heavily
dependent on the Dirac equation. The Dirac equation has been solved in recent
years for various potentials, as seen in literature [9–15]. The analytical
solutions of the Cornell potential with identical scalar and vector potentials
to the Dirac equation are examined in [9,10] using the perturbation method and
ansatz approach. For the modified-Hylleraas potential under spin and pseudo
spin symmetry limitations, the bound energy spectrum and corresponding
generalised hypergeometric wave function of the Dirac equation are found in
[5] using the Alhaidari formalism. The Nikiforov-Uvarov approach is used in
[11–13] to derive analytically the Dirac equation’s solutions with
pseudoscalar Cornell, Hartmann, and extended Hulthen potentials. Xian-Quen et
al. [12] solved the Dirac equation by using a new ring-shaped non-spherical
harmonic oscillator where the scalar and vector potentials are equivalent. The
Dirac equation for a relativistic electron is generally known as one of the
fundamental elements of both Standard Model (SM) and quantum electrodynamics
(QED) [14,15]. Both of them are employed to look for a new physical meaning
beyond the SM and to assess the viability of SM. Although the Dirac equation
was intended to explain electrons, it also successfully represents muons,
tayons, and quarks. It is astounding that the Dirac equation (DE) can
accurately describe quarks given that they are not visible in our physical
space and time. DE is utilized in phenomenological hadron models and quantum
chromodynamics (QCD) [15–20] to estimate the characteristics of heavy and
light baryons, where there are discrepancies between theoretical predictions
and experimental facts derived from quark contributions and from solving the
Dirac equation

The objective of this study is to provide the fractional Dirac model by
simplifying the DE to match the Schrodinger equation. By using the fractional
form of DE, several solutions are provided for the physical difficulties that
have been described above.

The following is how the paper is arranged: The fractional Nikiforov-Uvarov
(NU) approach, which is the method employed in the current research, is
briefly presented in Section 2. Both of energy eigenvalues and wave functions
of the fractional DE are computed in Section 3. The summary and conclusion are
reported in Section 4.

##  II The Fractional NU (FNU) method

This section provides a brief explanation of the FNU method for solving the
fractional differential equation in the sense of AKFD (see [7, 21] for more
details), which is written as follows:

$\mathcal{D}^{\alpha}\left[\mathcal{D}^{\alpha}\Upsilon(s)\right]+\frac{\bar{\nu}(s)}{\mu(s)}\mathcal{D}^{\alpha}\Upsilon(s)+\frac{\tilde{\mu}(s)}{\mu^{2}(s)}\Upsilon(s)=0,$
(2)

where $\mu(s)$ and $\tilde{\mu}(s)$ are the polynomials of maximum $2$nd
degree of $\alpha,2\alpha,$ respectively, and $\bar{\nu}(s)$ is a polynomial
of maximum degree of $\alpha$

where

$\mathcal{D}^{\alpha}\Upsilon(s)=Is^{1-\alpha}\Upsilon^{\prime}(s),$ (3)

$\mathcal{D}^{\alpha}\left[\mathcal{D}^{\alpha}\Upsilon(s)\right]=I^{2}\left[\left(1-\alpha\right)s^{1-2\alpha}\Upsilon^{\prime}(s)+s^{2-2\alpha}\Upsilon^{"}(s)\right].$
(4)

where

$I=\frac{\Gamma\left(\beta\right)}{\Gamma\left(\beta-\alpha+1\right)}$

where $0<\alpha\leq 1$ and $0<\beta\leq 1$. We substitute Eqs. (3) and (4)
into Eq. (2) to have:

$\Upsilon^{\prime\prime}(s)+\frac{\bar{\nu}_{h}(s)}{\mu_{h}(s)}\Upsilon^{\prime}(s)+\frac{\tilde{\mu}_{h}(s)}{\mu_{h}^{2}(s)}\Upsilon(s)=0,$
(5)

where
$\bar{\nu}_{h}(s)=\left(1-\alpha\right)s^{-\alpha}\mu(s)+I^{-2}\bar{\nu}(s);\mu_{h}(s)=s^{1-\alpha}\mu(s);\tilde{\mu}_{h}(s)=I^{-2}\tilde{\mu}(s).$
To find the particular solution of Eq. (5) by separation of variables, we deal
with the following transformation:

$\Upsilon(s)=\Theta(s)\Xi(s),$ (6)

which reduces to the following hypergeometric-type equation:

$\mu_{h}(s)\Xi^{\prime\prime}(s)+\nu_{h}(s)\Xi^{\prime}(s)+\Omega\Xi(s)=0,$
(7)

where

$\mu_{h}(s)=\Pi_{h}(s)\frac{\Theta(s)}{\Theta^{\prime}(s)},$ (8)
$\nu_{h}(s)=\bar{\nu}_{h}(s)+2\Pi_{h}(s);~{}\ \ \nu_{h}^{\prime}(s)<0,$ (9)

and

$\Omega=\Omega_{m}=-m\nu_{h}^{\prime}(s)-\frac{m(m-1)}{2}\mu_{h}^{\prime\prime}(s),m=0,1,2,...$
(10)

$\Xi(s)=\Xi_{m}(s)$ is a polynomial of $m$ degree, satisfying Eq. (7), which
is written as:

$\Xi_{m}(s)=\frac{N_{m}}{\varrho_{m}}\frac{d^{m}}{ds^{m}}(\mu_{h}^{\prime\prime}(s)\varrho(s)),$
(11)

where the normalization constant is $N_{m}$, and the wight function is
$\varrho(s)$ that satisfies:

$\frac{d}{ds}\eta(s)=\frac{\nu(s)}{\mu_{h}(s)}\eta(s);\ \ \
\eta(s)=\mu_{h}(s)\varrho(s),$ (12)
$\Pi_{h}(s)=\frac{\mu_{h}^{\prime}(s)-\bar{\nu}_{h}(s)}{2}\pm\sqrt{(\frac{\mu_{h}^{\prime}(s)-\bar{\nu}_{h}(s)}{2})^{2}-\tilde{\mu}_{h}(s)+\aleph\mu_{h}(s),}$
(13)

and

$\Omega=\aleph+\Pi_{h}^{\prime}(s),$ (14)

where the polynomial of $1$st degree is $\Pi_{h}(s)$. The $\aleph$ value in
Eq. (13) can possibly be calculated if we have square of expressions under the
square root of Eq. (13). This computation can be done if we have a
discriminant of zero.

##  III The DE for the Cornell Potential

The quark mass, represented by $\omega_{\alpha}$ with index $\alpha$ which
indicates the particle’s kind where in our study: $u$, $d$, and $s$ quark in
the presence of a confining potential $\mathcal{V}(r)$ in the DE is given
$\left[22\right]$

$\left[\mathbf{\alpha}\cdot\mathbf{\mathcal{P}+}\beta\omega_{\alpha}+\frac{1}{2}(1+\beta)\mathcal{V}(r)\right]\Upsilon(\mathbf{r})=\mathcal{E}_{\alpha
m}\Upsilon(\mathbf{r}),$ (15)

where the usual DE matrices are denoted by both $\mathbf{\alpha}$ and $\beta$.
Then, we decompose Eq. (15) in spherical coordinates. The following is the
obtained wave function component:

$\Upsilon(\mathbf{r})=\left({}_{\Theta(\mathbf{r})}^{\Xi(\mathbf{r})}\right)=\frac{1}{r}\left({}_{iv(r)\Psi_{-q}^{n}\left(\Phi,\Theta\right)}^{u(r)\Psi_{q}^{n}\left(\Phi,\Theta\right)}\right)\text{,}$
(16)

We substitute Eq. (16) into Eq. (15) and then separate its radial parts. Then,
we get:

$\frac{du(r)}{dr}=-\frac{q}{r}u(r)+\left[\mathcal{E}_{\alpha
m}+\omega_{\alpha}\right]v(r),$ (17)

$\frac{dv(r)}{dr}=\frac{q}{r}v(r)-\left[\mathcal{E}_{\alpha
m}-\omega_{\alpha}-\mathcal{V}(r)\right]u(r),$ (18)

where the $\mathcal{E}_{\alpha m}$ is an energy eigenvalue of particle
$\alpha$ and quantum number $q$, which is related to the total angular
momentum quantum number $\kappa$ as follows:

$q=\left\\{{}_{\left(\kappa+\frac{1}{2}\right)=l\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \text{ if
}~{}\kappa=l-\frac{1}{2}}^{-\left(\kappa+\frac{1}{2}\right)=-(l+1)\ \ \ \ \ \
\ \text{ if }~{}\kappa=l+\frac{1}{2}}\right.$ (19)

Eqs. (17) and (18) are reduced to a like Schrodinger equation as in
$\left[22\right]$ as follows

$[\frac{d^{2}}{dr^{2}}-\frac{q(q+1)}{r^{2}}+2\varepsilon_{0}(\varepsilon_{1}-\mathcal{V}(r))]u(r)=0$
(20)

where $\varepsilon_{0}=\frac{1}{2}\left(\mathcal{E}_{\alpha
m}+\omega_{\alpha}\right)$ and $\varepsilon_{1}=\left(\mathcal{E}_{\alpha
m}-\omega_{\alpha}\right)$. Let us take the Cornell potential as follows:

$\mathcal{V}(r)=fr-\frac{g}{r},$ (21)

where arbitrary positive constants $f$ and $g$ are used. The potential has
distinctive features, including a $1$st term that represents the confinement
force and a $2$nd term that characterizes the Colombo force. Eq. (21) is
substituted into Eq. (20) to yield

$[\frac{d^{2}}{dr^{2}}+2\varepsilon_{0}(\varepsilon_{1}-fr+\frac{g}{r}-\frac{q(q+1)}{2\varepsilon_{0}r^{2}})]u(r)=0.$
(22)

We suppose that $r=\frac{1}{x}$, and the characteristic radius of the meson is
presented by $r_{0}$. Therefore, this scheme depends on expanding
$\frac{1}{x}$ in a power series around $r_{0},$ i. e. around
$\delta=\frac{1}{r_{0}}$ in $x$ space (see [2] for more details). Eq. (22) can
be written as:

$[\frac{d^{2}}{dx^{2}}+\frac{2x}{x^{2}}\frac{d}{dx}+\frac{2}{x^{4}}(-\mathcal{D}_{1}+\mathcal{D}_{2}x-\mathcal{D}_{3}x^{2})]u(x)=0,$
(23)

where, $\mathcal{D}_{1}=-\varepsilon_{0}(\varepsilon_{1}-\frac{3f}{\delta})$,
$\mathcal{D}_{2}=\varepsilon_{0}(\frac{3f}{\delta^{2}}+g)$, and
$\mathcal{D}_{3}=\varepsilon_{0}(\frac{f}{\delta^{3}}+\frac{q(q+1)}{2\varepsilon_{0}})$.
To transfer Eq. $\left(23\right)$ to the fractional form, one uses
dimensionless form by taking $y=Ax$ where $A$ equals 1 GeV.

$[\frac{d^{2}}{dy^{2}}+\frac{2y}{y^{2}}\frac{d}{dy}+\frac{2}{y^{4}}(-\mathcal{D}_{11}+\mathcal{D}_{22}y-\mathcal{D}_{3}y^{2})]R(y)=0,$
(24)

where

$\mathcal{D}_{11}=\frac{\mathcal{D}_{1}}{A^{2}},\mathcal{D}_{22}=\frac{\mathcal{D}_{2}}{A}.$
(25)

From $\left[22\right],$ Eq. 24 can be written as:

$[\mathcal{D}^{\alpha}\left[\mathcal{D}^{\alpha}R(y)\right]+\frac{2y^{\alpha}}{y^{2\alpha}}\mathcal{D}^{\alpha}R(y)+\frac{2}{y^{4\alpha}}(-\mathcal{D}_{11}+\mathcal{D}_{22}y^{\alpha}-\mathcal{D}_{3}y^{2\alpha})]R(y)=0.$
(26)

We substitute Eqs. (3) and (4) into Eq. (26) to get:

$R^{\prime\prime}(y)+\frac{\bar{\nu}_{h}(y)}{\mu_{h}(y)}R^{\prime}(x)+\frac{\tilde{\mu}_{h}(y)}{\mu_{h}^{2}(y)}R(y)=0,$
(27)

where

$\bar{\nu}_{h}(s)=\left(1-\alpha\right)y^{\alpha}+2I^{-2}y^{\alpha},\mu_{h}(s)=y^{\alpha+1},\text{and
}\tilde{\mu}_{h}(y)=2I^{-2}(-\mathcal{D}_{1}+\mathcal{D}_{2}y^{\alpha}-\mathcal{D}_{3}y^{2\alpha}).$
(28)

Thus, Eq. (27) satisfies Eq. (5).
By substituting Eq. (28) into Eq. (13), we have:

$\Pi_{h}=-y^{\alpha}+\alpha I^{-2}y^{\alpha}\pm\sqrt{\left(-y^{\alpha}+\alpha
I^{-2}y^{\alpha}\right)^{2}-2I^{-2}(-\mathcal{D}_{11}+\mathcal{D}_{22}y^{\alpha}-\mathcal{D}_{3}y^{2\alpha})+\aleph
y^{1+\alpha}}.$ (29)

The constant $\aleph$ is selected in a way that there is a function under the
square root which has a double zero, where its discriminant equals $0$.
Therefore, we obtain:

$\aleph=\left(\frac{I^{-2}\mathcal{D}_{22}^{2}}{2\mathcal{D}_{11}}-(1-2\alpha
I^{-2}+\alpha^{2}I^{-4}+2I^{-2}\mathcal{D}_{3})\right)y^{\alpha-1}\text{.}$
(30)

We substitute Eq. (30) into Eq. (29) to obtain:

$\Pi_{h}\left(y\right)=-y^{\alpha}+\alpha
I^{-2}y^{\alpha}+\frac{\mathcal{D}_{22}}{\sqrt{2\mathcal{D}_{11}}}y^{\alpha}-\sqrt{2\mathcal{D}_{11}}$
(31)

From $\left[23\right]$, the Eq. (31) positive sign is found.
From Eq. (9), we get:

$\nu_{h}(y)=\left(1-\alpha\right)y^{\alpha}+2y^{\alpha}-2\left(\frac{\mathcal{D}_{22}}{\sqrt{2\mathcal{D}_{11}}}y^{\alpha}-\sqrt{2\mathcal{D}_{11}}\right),$
(32)

and from Eq. (10), we have:

$\Omega_{m}=\left(-m\left(3\alpha-\alpha^{2}\right)-\frac{2m\mathcal{D}_{22}\alpha}{\sqrt{2\mathcal{D}_{11}}}-\frac{m\left(m-1\right)\alpha\left(\alpha+1\right)}{2}\right)y^{\alpha-1}\text{.}$
(33)

According to Eq. (10), $\Omega=\Omega_{m}$. Therefore, the Eq. (33) energy
eigenvalues in the $N$-dimensional space is written as:

$\displaystyle\mathcal{E}_{mL}^{M}$
$\displaystyle=\frac{3f}{\delta}-\frac{2\varepsilon_{0}I^{-4}(\frac{3f}{\delta^{2}}+g)^{2}}{[\left(2m+1\right)\alpha+\sqrt{\left(2m+1\right)^{2}\alpha^{2}-4I^{-2}W}]^{2}}.$
(34)

with

$W=m\left(3\alpha-\alpha^{2}\right)+\frac{1}{2}m\left(m-1\right)\alpha\left(\alpha+1\right)-(1-2\alpha
I^{-2}+\alpha^{2}I^{-4}+2I^{-2}\mathcal{D}_{3})-\alpha+\alpha^{2}I^{-2}.$ (35)

The wave function’s radial is written as follows:

$R_{mL}\left(r^{\alpha}\right)=C_{mL}~{}r^{\left(-\frac{\mathcal{D}_{2}}{\sqrt{2\mathcal{D}_{1}}}-1\right)\alpha}e^{\sqrt{2\mathcal{D}_{1}}r^{\alpha}}(-r^{2\alpha}\mathcal{D}^{\alpha})^{m}(r^{\left(-2m+\frac{\mathcal{D}_{2}}{\sqrt{2\mathcal{D}_{1}}}\right)\alpha}e^{-2\sqrt{2\mathcal{D}_{1}}r^{\alpha}}).$
(36)

The normalization constant is denoted by $C_{mL}$ which is computed by
$\int\left|R_{mL}\left(r^{\alpha}\right)\right|^{2}dr=1$. Eq. (36) is not
explicitly dependent on the dimensions’ number.
$\int\left|R_{mL}\left(r\right)\right|^{2}dr=1$ stays the same without any
change. Therefore, Eq. (36) is reduced to a special case in $\left[23\right]$
at $\alpha=\beta=1$ and $c=0$

$\varepsilon_{1}=\frac{3f}{\delta}-\frac{2\varepsilon_{0}(\frac{3f}{\delta^{2}}+g)^{2}}{[(2m+1)\pm\sqrt{1+\frac{8\varepsilon_{0}f}{\delta^{3}}+4q(q+1)}]^{2}}\text{.}$
(37)

##  IV Summary and Conclusion

The AKFD, which has more benefits than other classical fractional derivatives,
is used in connection with the fractional Nikiforov-Uvarov approach to solve
the relativistic Dirac equation after being reduced to a like the Schrodinger
equation which incorporates the Cornell interaction potential that is used to
produce the energy eigenvalues and associated wave functions in fractional
forms. The ability to describe interactions over both short and long distances
is well-established by the Cornell potential. The current results at
$\alpha=\beta=1$ are used as a special case to generate the classical results.
The use of the Nikiforov-Uvarov approach and the AKFD in the current work has
the benefit that the fractional solution of Dirac is not taken into account in
many recent publications. In addition, the conclusion from the current study
is crucial for enhancing and resolving those from classical relativistic
quantum systems.

##  V References

  1. 1.

M. Abu-Shady, Sh Y. Ezz-Alarab, Conformable Fractional of the Analytical Exact
Iteration Method for Heavy Quarkonium Masses Spectra, Few-Body Systems 62, 1,
(2021).

  2. 2.

M. Abu-Shady, Quarkonium masses in a hot QCD medium using conformable
fractional of the Nikiforov–Uvarov method, International Journal of Modern
Physics A 34, 1950201 (2019).

  3. 3.

M. Abu-Shady, E. M. Khokha, T. A. Abdel-Karim, The generalized fractional NU
method for the diatomic molecules in the Deng–Fan model, The European Physical
Journal D 76.9 (2022): 159.

  4. 4.

M. Abu-shady, H. M. Fath-Allah, Masses of Single, Double, and Triple Heavy
Baryons in the Hyper-Central Quark Model by Using GF-AEIM, Advances in High
Energy Physics 2022 (2022).

  5. 5.

A. D. Alhaidari, H. Bahlouli, A. Al-Hasan, Phys. Lett. A 349, 87 (2006).

  6. 6.

L. A. Trevisan, Carlos Mirez, F. M. Andrade, Few-body Syst. 55 1055 (2014).

  7. 7.

M. Abu-Shady, M. K. A. Kaabar, A Generalized Definition of the Fractional
Derivative with Applications, Mathematical Problems in Engineering, vol. 2021,
9444803, (2021).

  8. 8.

H. Hassanabadi, E. Maghsoodi, Akpan N. Ikot, S. Zarrinkamar, Adv. High Energ.
Phys. 2014, 831938 (2014).

  9. 9.

A. N. Ikot, E. Maghsoodi, O. A. Awoga, S. Zarrinkamar, H. Hassanabadi, Quant.
Phys. Lett. 3, 7 (2014).

  10. 10.

M. Hamzavi, A. A. Rajabi, Chinese Phys. C 37, 103102 (2013).

  11. 11.

M. Hamzavi, H. Hassanabadi, A. A. Rajabi, Inter. J. Mod. Phys. E, 19, 2189
(2010).

  12. 12.

H. Xian-Quen, L. Guoug, W. Yhi-Min, N. Lion-Bin, M. Yan. Commun. Theor. Phys.
53, 242 (2010).

  13. 13.

A. Arda, R. Sever, C. Tezcan, Cent. Eur. J. Phys. 8, 843 (2010).

  14. 14.

N.N. Bogoliubov, A.A. Logunov, A.I. Oksak, I.T. Todorov, General principles of
quantum field theory. Moscow, Nauka, 1987 (in Russian).

  15. 15.

F. J. Yndurain, Quantum Chromodynamics. Springer-Verlag, New York, Berlin-
Heidelberg-Tokyo, 1983.

  16. 16.

M. Abu-Shady, Chiral Logarithmic Quark Model of N and $\Delta$ with an A-Term
in the Mean-Field Approximation, International Journal of Modern Physics A
26.02 (2011): 235-249.

  17. 17.

M. Abu-Shady, Meson properties at finite temperature in the linear sigma
model, International Journal of Theoretical Physics 49 (2010): 2425-2436.

  18. 18.

M. Abu-Shady, M. Soleiman, The extended quark sigma model at finite
temperature and baryonic chemical potential, Physics of Particles and Nuclei
Letters 10 (2013): 683-692.

  19. 19.

M. Abu-Shady, Effect of logarithmic mesonic potential on nucleon properties,
Modern Physics Letters A 24.20 (2009): 1617-1629.

  20. 20.

M. Abu-Shady, Nucleon Properties Below the Critical Point Temperature,
International Journal of Theoretical Physics 50 (2011): 1372-1381

  21. 21.

H. Karayer, D. Demirhan, F. Büyükk, Commun. Theor. Phys. 66, 12 (2018).

  22. 22.

L. A. Trevisan, Carlos Mirez, F. M. Andrade, Few-body Syst. 55 1055 (2014).

  23. 23.

M. Abu-Shady, Analytic solution of Dirac Equation for extended Cornell
Potential using the Nikiforov-Uvarov method, Boson Journal of Modern Physics,
1, 1, 61, arXiv:1507.03706 (2015).

  24. 24.

F. Martínez, M. K. A. Kaabar, A Novel theoretical investigation of the Abu-
Shady–Kaabar fractional derivative as a modeling tool for science and
engineering, Computational and Mathematical Methods in Medicine, vol. 2022,
4119082, (2022).