# Testing Probabilistic Circuits ††thanks: The accompanying tool, available
open source, can be found at https://github.com/meelgroup/teq. The Appendix is
available in the accompanying supplementary material. ††thanks: The authors
decided to forgo the old convention of alphabetical ordering of authors in
favor of a randomized ordering, denoted by ⓡ. The publicly verifiable record
of the randomization is available at
https://www.aeaweb.org/journals/policies/random-author-order/search with
confirmation code: icoxrj0sNB2L. For citation of the work, authors request
that the citation guidelines by AEA for random author ordering be followed.

Yash Pote ⓡ Kuldeep S. Meel
School of Computing, National University of Singapore

###### Abstract

Probabilistic circuits (PCs) are a powerful modeling framework for
representing tractable probability distributions over combinatorial spaces. In
machine learning and probabilistic programming, one is often interested in
understanding whether the distributions learned using PCs are close to the
desired distribution. Thus, given two probabilistic circuits, a fundamental
problem of interest is to determine whether their distributions are close to
each other.

The primary contribution of this paper is a closeness test for PCs with
respect to the total variation distance metric. Our algorithm utilizes two
common PC queries, counting and sampling. In particular, we provide a poly-
time probabilistic algorithm to check the closeness of two PCs, when the PCs
support tractable approximate counting and sampling. We demonstrate the
practical efficiency of our algorithmic framework via a detailed experimental
evaluation of a prototype implementation against a set of 475 PC benchmarks.
We find that our test correctly decides the closeness of all 475 PCs within
3600 seconds.

##  1 Introduction

Probabilistic modeling is at the heart of modern computer science, with
applications ranging from image recognition and image generation [29, 30] to
weather forecasting [3]. Probabilistic models have a multitude of
representations, such as probabilistic circuits (PCs) [9], graphical models
[19], generative networks [16], and determinantal point processes [20]. Of
particular interest to us are PCs, which are known to support guaranteed
inference and thus have applications in safety-critical fields such as
healthcare [2, 25]. In this work, we will focus on PCs that are fragments of
the Negation Normal Form ($\mathsf{NNF}$), specifically $\mathsf{DNNF}$s,
$\mathsf{d}$-$\mathsf{DNNF}$s, $\mathsf{SDNNF}$s, and $\mathsf{PI}$s [13]. We
refer to the survey by Choi et al. [9] for more details regarding PCs.

Given two distributions $P$ and $Q$, a fundamental problem is to determine
whether they are close. Closeness between distributions is frequently
quantified using the total variation (TV) distance,
$d_{TV}(P,Q)=(1/2)\|P-Q\|_{1},$ where $\|\cdot\|$ is the $\ell_{1}$ norm [21,
6]. Thus, stated formally, closeness testing is the problem of deciding
whether $d_{TV}(P,Q)\leq\varepsilon$ or $d_{TV}(P,Q)\geq\eta$ for
$0\leq\varepsilon<\eta\leq 1$. Determining the closeness of models has
applications in AI planning [13], bioinformatics [31, 33, 35] and
probabilistic program verification [15, 23].

Equivalence testing is a special case of closeness testing, where one tests if
$d_{TV}(P,Q)=0$. Darwiche and Huang [13] initiated the study of equivalence
testing of PCs by designing an equivalence test for
$\mathsf{d}$-$\mathsf{DNNF}$s. An equivalence test is, however, of little use
in contexts where the PCs under test encode non-identical distributions that
are nonetheless close enough for practical purposes. Such situations may arise
due to the use of approximate PC compilation [10] and sampling-based learning
of PCs [26, 27]. As a concrete example, consider PCs that are learned via
approximate methods such as stochastic gradient descent [27]. In such a case,
PCs are likely to converge to close but non-identical distributions. Given two
such PCs, we would like to know whether they have converged to distributions
close to each other. Thus, we raise the question: Does there exist an
efficient algorithm to test the closeness of two PC distributions?

In this work, we design the first closeness test for PCs with respect to TV
distance, called $\mathsf{Teq}$. Assuming the tested PCs allow poly-time
approximate weighted model counting and sampling, $\mathsf{Teq}$ runs in
polynomial time. Formally, given two PC distributions $P$ and $Q$, and three
parameters ($\varepsilon$,$\eta$,$\delta$), for closeness($\varepsilon$),
farness($\eta$), and tolerance($\delta$), $\mathsf{Teq}$ returns
$\mathsf{Accept}$ if $d_{TV}(P,Q)\leq\varepsilon$ and $\mathsf{Reject}$ if
$d_{TV}(P,Q)\geq\eta$ with probability at least $1-\delta$. $\mathsf{Teq}$
makes atmost $O((\eta-\varepsilon)^{-2}\log(\delta^{-1}))$ calls to the
sampler and exactly 2 calls to the counter.

$\mathsf{Teq}$ builds on a general distance estimation technique of Canonne
and Rubinfeld [4] that estimates the distance between two distributions with a
small number of samples. In the context of PCs, the algorithm requires access
to an exact sampler and an exact counter. Since not all PCs support exact
sampling and counting, we modify the technique presented in [4] to allow for
approximate samples and counts. Furthermore, we implement and test
$\mathsf{Teq}$ on a dataset of publicly available PCs arising from
applications in circuit testing. Our results show that closeness testing can
be accurate and scalable in practice.

For some $\mathsf{NNF}$ fragments, such as $\mathsf{DNNF}$, no sampling
algorithm is known, and for fragments such as $\mathsf{PI}$, sampling is known
to be NP-hard [32]. Since $\mathsf{Teq}$ requires access to approximate
weighted counters and samplers to achieve tractability, the question of
determining the closeness of the PCs mentioned above remains unanswered. Thus,
we investigate further and characterize the complexity of closeness testing
for a broad range of PCs. Our characterization reveals that PCs from the
fragments $\mathsf{d}$-$\mathsf{DNNF}$s and $\mathsf{SDNNF}$s can be tested
for closeness in poly-time via $\mathsf{Teq}$, owing to the algorithms of
Darwiche [11] and Arenas et al. [1]. We show that the $\mathsf{SDNNF}$
approximate counting algorithm of Arenas et al. [1] can be extended to log-
linear $\mathsf{SDNNF}$s using chain formulas [8]. Then, using previously
known results, we also find that there are no poly-time equivalence tests for
PCs from $\mathsf{PI}$ and $\mathsf{DNNF}$, conditional on widely believed
complexity-theoretic conjectures. Our characterization also reveals some open
questions regarding the complexity of closeness and equivalence testing of
PCs.

The rest of the paper is organized in the following way. We define the
notation and discuss related work in Section 2. We then present the main
contribution of the paper, the closeness test $\mathsf{Teq}$, and the
associated proof of correctness in Section 3. We present our experimental
findings in Section 4, and then discuss the complexity landscape of closeness
testing in Section 5. We conclude the paper and discuss some open problems in
Section 6. Due to space constraints, we defer some proofs to the supplementary
Section A.

##  2 Background

Let $\varphi:\\{0,1\\}^{n}\rightarrow\\{0,1\\}$ be a circuit over $n$ Boolean
variables. An assignment $\sigma\in\\{0,1\\}^{n}$ to the variables of
$\varphi$ is a satisfying assignment if $\varphi(\sigma)=1$. The set of all
satisfying assignments of $\varphi$ is $R_{\varphi}$. If $|R_{\varphi}|>0$,
then $\varphi$ is said to be _satisfiable_ and if $|R_{\varphi}|=2^{n}$, then
$\varphi$ is said to be _valid_. We use $|\varphi|$ to denote the size of
circuit $\varphi$, where the size is the total number of vertices and edges in
the circuit DAG.

The polynomial hierarchy (PH) contains the classes $\Sigma_{1}^{\text{P}}$
(NP) and $\Pi_{1}^{\text{P}}$ (co-NP) along with generalizations of the form
$\Sigma_{i}^{\text{P}}$ and $\Pi_{i}^{\text{P}}$ where
$\Pi^{\text{P}}_{i+1}=\text{co-NP}^{\Pi_{i}^{P}}$ and
$\Sigma_{i+1}^{P}=\text{NP}^{\Sigma_{i}^{P}}$ [34]. The classes
${\Sigma_{i}^{P}}$ and ${\Pi_{i}^{P}}$ are said to be at level $i$. If it is
shown that two classes on the same or consecutive levels are equal, the
hierarchy collapses to that level. Such a collapse is considered unlikely, and
hence is used as the basic assumption for showing hardness results, including
the ones we present in the paper.

###  2.1 Probability distributions

A weight function $\mathtt{w}:\\{0,1\\}^{n}\rightarrow\mathbb{Q}^{+}$ assigns
a positive rational weight to each assignment $\sigma$. We extend the
definition of $\mathtt{w}$ to also allow circuits as input:
$\mathtt{w}(\varphi)=\underset{\sigma\in
R_{\varphi}}{\sum}\mathtt{w}(\sigma)$. For weight function $\mathtt{w}$ and
circuit $\varphi$, $\mathtt{w}(\varphi)$ is the weighted model count (WMC) of
$\varphi$ w.r.t. $\mathtt{w}$.

In this paper, we focus on log-linear weight functions as they capture a wide
class of distributions, including those arising from graphical models,
conditional random fields, and skip-gram models [24]. Log-linear models are
represented as literal-weighted functions, defined as:

######  Definition 1.

For a set $X$ of $n$ variables, a weight function $\mathtt{w}$ is called
literal-weighted if there is a poly-time computable map
$\mathtt{w}:X\rightarrow\mathbb{Q}\cap(0,1)$ such that for any assignment
$\sigma\in\\{0,1\\}^{n}:$

$\displaystyle\mathtt{w}(\sigma)=\prod_{x\in\sigma}\begin{cases}\mathtt{w}(x)&if\quad
x=1\\\ 1-\mathtt{w}(x)&if\quad x=0\end{cases}$

For all circuits $\varphi$, and log-linear weight functions $\mathtt{w}$,
$\mathtt{w}(\varphi)$ can be represented in size polynomial in the input.

##### Probabilistic circuits:

A probabilistic circuit is a satisfiable circuit $\varphi$ along with a weight
function $\mathtt{w}$. $\varphi$ and $\mathtt{w}$ together define a discrete
probability distribution on the set $\\{0,1\\}^{n}$ that is supported over
$R_{\varphi}$. We denote the p.m.f. of this distribution as:
$P(\varphi,\mathtt{w})(\sigma)=\begin{cases}0&\varphi(\sigma)=0\\\
\mathtt{w}(\sigma)/\mathtt{w}(\varphi)&\varphi(\sigma)=1\end{cases}$

In this paper, we study circuits that are fragments of the Negation Normal
Form ($\mathsf{NNF}$). A circuit $\varphi$ in $\mathsf{NNF}$ is a rooted,
directed acyclic graph (DAG), where each leaf node is labeled with true,
false, $v$ or $\lnot v$; and each internal node is labeled with a $\wedge$ or
$\vee$ and can have arbitrarily many children. We focus on four fragments of
$\mathsf{NNF}$, namely, Decomposable $\mathsf{NNF}$($\mathsf{DNNF}$),
deterministic-$\mathsf{DNNF}$($\mathsf{d}$-$\mathsf{DNNF}$), Structured
$\mathsf{DNNF}$($\mathsf{SDNNF}$), and Prime Implicates($\mathsf{PI}$). For
further information regarding circuits in $\mathsf{NNF}$, refer to the survey
[14] and the paper [28].

The TV distance of two probability distributions
$P(\varphi_{1},\mathtt{w_{1}})$ and $P(\varphi_{2},\mathtt{w_{2}})$ over
$\\{0,1\\}^{n}$ is defined as:
$d_{TV}(P(\varphi_{1},\mathtt{w_{1}}),P(\varphi_{2},\mathtt{w_{2}}))=\frac{1}{2}\sum_{\sigma\in\\{0,1\\}^{n}}|P(\varphi_{1},\mathtt{w_{1}})(\sigma)-P(\varphi_{2},\mathtt{w_{2}})(\sigma)|$.

$P(\varphi_{1},\mathtt{w_{1}})$ and $P(\varphi_{2},\mathtt{w_{2}})$ are said
to be (1) equivalent if
$d_{TV}(P(\varphi_{1},\mathtt{w_{1}}),P(\varphi_{2},\mathtt{w_{2}}))=0$, (2)
$\varepsilon$-close if
$d_{TV}(P(\varphi_{1},\mathtt{w_{1}}),P(\varphi_{2},\mathtt{w_{2}}))\leq\varepsilon$,
and (3) $\eta$-far if
$d_{TV}(P(\varphi_{1},\mathtt{w_{1}}),P(\varphi_{2},\mathtt{w_{2}}))\geq\eta$.

Our closeness testing algorithm $\mathsf{Teq}$, assumes access to an
approximate weighted counter $\mathsf{Awct}(\alpha,\beta,\varphi,\mathtt{w})$,
and an approximate weighted sampler
$\mathsf{Samp}(\alpha,\beta,\varphi,\mathtt{w})$. We define their behavior as
follows:

######  Definition 2.

$\mathsf{Awct}(\alpha,\beta,\varphi,\mathtt{w})$ takes a circuit $\varphi$, a
weight function $\mathtt{w}$, a tolerance parameter $\alpha>0$ and a
confidence parameter $\beta>0$ as input and returns the approximate weighted
model count of $\varphi$ w.r.t. $\mathtt{w}$ such that

$\displaystyle\Pr\left[\frac{\mathtt{w}(\varphi)}{1+\alpha}\leq{\mathsf{Awct}}(\alpha,\beta,\varphi,\mathtt{w})\leq(1+\alpha)\mathtt{w}(\varphi)\right]\geq
1-\beta$

Tractable approximate counting algorithms for PCs are known as Fully
Polynomial Randomised Approximation Schemes (FPRAS). The running time of an
FPRAS is given by
$T(\alpha,\beta,\varphi)=poly(\alpha^{-1},\log(\beta^{-1}),|\varphi|)$.

######  Definition 3.

$\mathsf{Samp}(\alpha,\beta,\varphi,\mathtt{w})$ takes a circuit $\varphi$, a
weight function $\mathtt{w}$, a tolerance parameter $\alpha>0$ and a
confidence parameter $\beta>0$ as input and returns either (1) a satisfying
assignment $\sigma$ sampled approximately w.r.t. weight function $\mathtt{w}$
with probability $\geq 1-\beta$ or (2) a symbol $\perp$ indicating failure
with probability $<\beta$. In other words, whenever $\mathsf{Samp}$ samples
$\sigma$:

$\displaystyle\frac{P(\varphi,\mathtt{w})(\sigma)}{1+\alpha}\leq\Pr[\mathsf{Samp}(\alpha,\beta,\varphi,\mathtt{w})=\sigma]\leq(1+\alpha)P(\varphi,\mathtt{w})(\sigma)$

Tractable approximate sampling algorithms for PCs are known as Fully
Polynomial Almost Uniform Samplers (FPAUS). The running time of an FPAUS for a
single sample is given by
$T(\alpha,\beta,\varphi)=poly(\alpha^{-1},\log(\beta^{-1}),|\varphi|)$.

In the rest of the paper $[m]$ denotes the set $\\{1,2,\ldots m\\}$,
$\mathbbm{1}(e)$ represents the indicator variable for event $e$, and
$\mathbbm{E}(v)$ represents the expectation of random variable $v$.

###  2.2 Related work

##### Closeness testing:

Viewing circuit equivalence testing through the lens of distribution testing,
we see that the $\mathsf{d}$-$\mathsf{DNNF}$ equivalence test of Darwiche and
Huang [13] can be interpreted as an equivalence test for uniform distribution
on the satisfying assignments of $\mathsf{d}$-$\mathsf{DNNF}$s. This
relationship between circuit equivalence testing and closeness testing lets us
rule out the existence of distributional equivalence tests for all those
circuits for which circuit equivalence is already known to be hard under
complexity-theoretic assumptions. We will explore this further in Section 5.2.

##### Distribution testing:

Discrete probability distributions are typically defined over an exponentially
large number of points; hence a lot of recent algorithms research has focused
on devising tests that require access to only a sublinear or even constant
number of points in the distribution [5]. In this work, we work with
distributions over $\\{0,1\\}^{n}$, and thus we aim to devise algorithms with
running time at most polynomial in $n$. Previous work in testing distributions
over Boolean functions has focused on the setting where the distributions
offer pair-conditional sampling access [7, 22]. Using pair-conditional
sampling access, Meel$ⓡ$ et al. [22] were able to test distributions for
closeness using $\tilde{O}(tilt(\varphi)^{2}/(\eta-6\varepsilon)^{2}\eta)$
queries, where $tilt$ is the ratio of the probabilities of the most and least
probable element in the support.

##  3 $\mathsf{Teq}$: a tractable algorithm for closeness testing

In this section, we present the main contribution of the paper: a closeness
test for PCs, $\mathsf{Teq}$. The pseudocode of $\mathsf{Teq}$ is given in
Algorithm 1.

Given satisfiable circuits $\varphi_{1},\varphi_{2}$ and weight functions
$\mathtt{w_{1}},\mathtt{w_{2}}$ along with parameters
$(\varepsilon,\eta,\delta)$, $\mathsf{Teq}$ decides whether the TV distance
between $P(\varphi_{1},\mathtt{w_{1}})$ and $P(\varphi_{2},\mathtt{w_{2}})$ is
lesser than $\varepsilon$ or greater than $\eta$ with confidence at least
$1-\delta$. $\mathsf{Teq}$ assumes access to an approximate weighted counter
$\mathsf{Awct}(\alpha,\beta,\varphi,\mathtt{w})$, and an approximate weighted
sampler $\mathsf{Samp}(\alpha,\beta,\varphi,\mathtt{w})$. We define their
behavior in the following two definitions.

##### The algorithm

$\mathsf{Teq}$ starts by computing constants $\gamma$ and $m$. Then it queries
the $\mathsf{Awct}$ routine with circuit $\varphi_{1}$ and weight function
$\mathtt{w_{1}}$ to obtain a $\sqrt{1+\gamma/4}-1$ approximation of
$\mathtt{w_{1}}(\varphi_{1})$ with confidence at least $1-\delta/8$. A similar
query is made for $\varphi_{2}$ and $\mathtt{w_{2}}$ to obtain an approximate
value for $\mathtt{w_{2}}(\varphi_{2})$. These values are stored in $k_{1}$
and $k_{2}$, respectively. $\mathsf{Teq}$ maintains a $m$-sized array
$\Gamma$, to store the estimates for $r(\sigma_{i})$. $\mathsf{Teq}$ now
iterates $m$ times. In each iteration, it generates one sample $\sigma_{i}$
through the $\mathsf{Samp}$ call on line 7. There is a small probability of at
most $\delta/4m$ that this call fails and returns $\perp$. $\mathsf{Teq}$ only
samples from one of the two PCs.

The algorithm then proceeds to compute the weight of assignment $\sigma_{i}$
w.r.t. the weight functions $\mathtt{w_{1}}$ and $\mathtt{w_{2}}$ and stores
it in $s_{1}$ and $s_{2}$, respectively. Using the weights and approximate
weighted counts stored in $k_{1},k_{2}$ the algorithm computes the value
$r(\sigma_{i})$ on line 10, where $r(\sigma_{i})$ is an approximation of the
ratio of the probability of $\sigma_{i}$ in the distribution
$P(\varphi_{2},\mathtt{w_{2}})$ to its probability in
$P(\varphi_{1},\mathtt{w_{1}})$. Since $\sigma_{i}$ was sampled from
$P(\varphi_{1},\mathtt{w_{1}})$, its probability in
$P(\varphi_{1},\mathtt{w_{1}})$ cannot be 0, ensuring that there is no
division by 0. If the ratio $r(\sigma_{i})$ is less than 1, then $\Gamma[i]$
is updated with the value $1-r(\sigma_{i})$ otherwise the value of $\Gamma[i]$
remains 0. After the $m$ iterations, $\mathsf{Teq}$ sums up the values in the
array $\Gamma$. If the sum is found to be less than threshold
$m(\varepsilon+\gamma)$, $\mathsf{Teq}$ returns $\mathsf{Accept}$ and
otherwise returns $\mathsf{Reject}$.

Algorithm 1
$\mathsf{Teq}(\varphi_{1},\mathtt{w_{1}},\varphi_{2},\mathtt{w_{2}},\varepsilon,\eta,\delta)$

1: $\gamma\leftarrow(\eta-\varepsilon)/2$

2: $m\leftarrow\lceil 2\log(4/\delta)/\gamma^{2}\rceil$

3: $\Gamma\leftarrow[0]*m$

4:
$k_{1}\leftarrow\mathsf{Awct}(\sqrt{1+\gamma/4}-1,\delta/8,\varphi_{1},\mathtt{w_{1}})$

5:
$k_{2}\leftarrow\mathsf{Awct}(\sqrt{1+\gamma/4}-1,\delta/8,\varphi_{2},\mathtt{w_{2}})$

6: for $i\in\\{1,2\ldots,m\\}$ do

7:
$\sigma_{i}\leftarrow\mathsf{Samp}(\gamma/(4\eta-2\gamma),\delta/4m,\varphi_{1},\mathtt{w_{1}})$

8: if $\sigma_{i}\not=\perp$ then

9:
$s_{1}\leftarrow\mathtt{w_{1}}(\sigma_{i}),s_{2}\leftarrow\mathtt{w_{2}}(\sigma_{i})$

10: $r(\sigma_{i})\leftarrow\frac{s_{2}}{k_{2}}\cdot\frac{k_{1}}{s_{1}}$

11: if $r(\sigma_{i})<1$ then

12: $\Gamma[i]\leftarrow 1-r(\sigma_{i})$

13: if $\sum_{i\in[m]}\Gamma[i]\leq m(\varepsilon+\gamma)$ then

14: Return $\mathsf{Accept}$

15: else

16: Return $\mathsf{Reject}$

The following theorem asserts the correctness of $\mathsf{Teq}$.

######  Theorem 1.

Given two satisfiable probabilistic circuits $\varphi_{1},\varphi_{2}$ and
weight functions $\mathtt{w_{1}},\mathtt{w_{2}}$, along with parameters
$\varepsilon<\eta<1$ and $\delta<1$,

  1. A.

If
$d_{TV}(P(\varphi_{1},\mathtt{w_{1}}),P(\varphi_{2},\mathtt{w_{2}}))\leq\varepsilon$,
then
$\mathsf{Teq}(\varphi_{1},\mathtt{w_{1}},\varphi_{2},\mathtt{w_{2}},\varepsilon,\eta,\delta)$
returns $\mathsf{Accept}$ with probability at least $(1-\delta)$.

  2. B.

If
$d_{TV}(P(\varphi_{1},\mathtt{w_{1}}),P(\varphi_{2},\mathtt{w_{2}}))\geq\eta$,
then
$\mathsf{Teq}(\varphi_{1},\mathtt{w_{1}},\varphi_{2},\mathtt{w_{2}},\varepsilon,\eta,\delta)$
returns $\mathsf{Reject}$ with probability at least $(1-\delta)$.

The following theorem states the running time of the algorithm,

######  Theorem 2.

Let $\gamma=\eta-\varepsilon$, then the time complexity of $\mathsf{Teq}$ is
in
$O\left(T_{\mathsf{Awct}}(\gamma,\delta,\max(|\varphi_{1}|,|\varphi_{2}|))+T_{\mathsf{Samp}}(\gamma,\delta,\max(|\varphi_{1}|,|\varphi_{2}|))\frac{\log(\delta^{-1})}{\gamma^{2}}\right)$.
If the underlying PCs support approximate counting and sampling in polynomial
time, then the running time of $\mathsf{Teq}$ is also polynomial in terms of
$\gamma,\log(\delta^{-1})$ and $max(|\varphi_{1}|,|\varphi_{2}|)$.

To improve readability, we use $P_{1}$ to refer to the distribution
$P(\varphi_{1},\mathtt{w_{1}})$ and $P_{2}$ to refer to
$P(\varphi_{2},\mathtt{w_{2}})$.

###  3.1 Proving the correctness of $\mathsf{Teq}$

In this subsection, we present the theoretical analysis of $\mathsf{Teq}$, and
the proof of Theorem 1(A). We will defer the proofs of Theorem 1(B) and
Theorem 2 to the supplementary Section A.4.2 and Section A.4.3, respectively.

For the purpose of the proof, we will first define events
$\mathtt{Pass_{1}},\mathtt{Pass_{2}}$ and $\mathtt{Good}$. Events
$\mathtt{Pass_{1}},\mathtt{Pass_{2}}$ are defined w.r.t. the function calls
$\mathsf{Awct}(\sqrt{1+\gamma/4}-1,\delta/8,\varphi_{1},\mathtt{w_{1}})$ and
$\mathsf{Awct}(\sqrt{1+\gamma/4}-1,\delta/8,\varphi_{2},\mathtt{w_{2}})$,
respectively (as on lines 4, 5 of Algorithm 1). $\mathtt{Pass_{1}}$ and
$\mathtt{Pass_{2}}$ represent the events that the two calls correctly return
$\sqrt{1+\gamma/4}$ approximations of the weighted model counts of
$\varphi_{1}$ and $\varphi_{2}$ i.e.
$\frac{\mathtt{w_{1}}(\varphi_{1})}{\sqrt{1+\gamma/4}}\leq\mathsf{Awct}(\sqrt{1+\gamma/4}-1,\delta/8,\varphi_{1},\mathtt{w_{1}})\leq(\sqrt{1+\gamma/4})\mathtt{w_{1}}(\varphi_{1})$,
and
$\frac{\mathtt{w_{2}}(\varphi_{2})}{\sqrt{1+\gamma/4}}\leq\mathsf{Awct}(\sqrt{1+\gamma/4}-1,\delta/8,\varphi_{2},\mathtt{w_{2}})\leq(\sqrt{1+\gamma/4})\mathtt{w_{2}}(\varphi_{2})$.
From the definition of $\mathsf{Awct}$, we have
$\Pr[\mathtt{Pass_{1}}],\Pr[\mathtt{Pass_{2}}]\geq 1-\delta/8$.

Let $\mathtt{Fail_{i}}$ denote the event that $\mathsf{Samp}$ (Algorithm 1,
line 7) returns the symbol $\perp$ in the $i$th iteration of the loop. By the
definition of $\mathsf{Samp}$ we know that
$\forall_{i\in[m]}\Pr[\mathtt{Fail_{i}}]<\delta/4m$.

The analysis of $\mathsf{Teq}$ requires that all $m$ $\mathsf{Samp}$ calls and
both $\mathsf{Awct}$ calls return correctly. We denote this super-event as
$\mathtt{Good}=\bigcap_{i\in[m]}\overline{\mathtt{Fail_{i}}}\cap\mathtt{Pass_{1}}\cap\mathtt{Pass_{2}}$.
Applying the union bound we see that the probability of all calls to
$\mathsf{Awct}$ and $\mathsf{Samp}$ returning without error is at least
$1-\delta/2$:

$\displaystyle\Pr[\mathtt{Good}]$
$\displaystyle=1-\Pr[\bigcup_{i\in[m]}\mathtt{Fail_{i}}\cup\overline{\mathtt{Pass_{1}}}\cup\overline{\mathtt{Pass_{2}}}]\geq
1-m\cdot\delta/4m-2\cdot\delta/8=1-\delta/2$ (1)

We will now state a lemma, which we will prove in the supplementary Section
A.4.

######  Lemma 1.

$\mathtt{Good}\rightarrow\left|r(\sigma)-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right|\leq\gamma/4\cdot\frac{P_{2}(\sigma)}{P_{1}(\sigma)}$

We now prove the lemma critical for our proof of correctness of
$\mathsf{Teq}$.

######  Lemma 2.

Assuming the event $\mathtt{Good}$, let
$A=\sum_{\sigma\in\\{0,1\\}^{n}}\mathbbm{1}\left(r(\sigma)<1\right)\left(1-r(\sigma)\right)P_{1}(\sigma)$
, then

  1. 1.

If $d_{TV}(P_{1},P_{2})\leq\varepsilon$ , then $A\leq\varepsilon+\gamma/4$

  2. 2.

If $d_{TV}(P_{1},P_{2})\geq\eta$ , then $A\geq\eta-\gamma/4$

###### Proof.

If $\sum_{x}\left(P_{1}(x)-P_{2}(x)\right)=0$, then
$\frac{1}{2}\sum_{x}|P_{1}(x)-P_{2}(x)|=\underset{x:P_{1}(x)-P_{2}(x)>0}{\sum}(P_{1}(x)-P_{2}(x))$.
Using this fact we see that,

$\displaystyle d_{TV}(P_{1},P_{2})$
$\displaystyle=\sum_{\sigma:P_{2}(\sigma)<P_{1}(\sigma)}P_{1}(\sigma)-P_{2}(\sigma)=\sum_{\sigma:\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1}\left(1-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right)P_{1}(\sigma)$
$\displaystyle=\sum_{\sigma\in\\{0,1\\}^{n}}\mathbbm{1}\left(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1\right)\left(1-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right)P_{1}(\sigma)$
$\displaystyle=A+\underbrace{\sum_{\sigma\in\\{0,1\\}^{n}}\mathbbm{1}\left(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1\right)\left(1-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right)P_{1}(\sigma)-A}_{B}$

Thus we have that $d_{TV}(P_{1},P_{2})-A=B$. We now divide the set of
assignments $\sigma\in\\{0,1\\}^{n}$ into three disjoint partition
$S_{1},S_{2}$ and $S_{3}$ as following:
$S_{1}=\\{\sigma:\mathbbm{1}(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1)=\mathbbm{1}(r(\sigma)<1)\\}$;
$S_{2}=\\{\sigma:\mathbbm{1}(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1)>\mathbbm{1}(r(\sigma)<1)\\}$;
$S_{3}=\\{\sigma:\mathbbm{1}(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1)<\mathbbm{1}(r(\sigma)<1)\\}$.
The definition implies that the indicator $\mathbbm{1}(r(\sigma)<1)$ is $0$
for all assignments in the set $S_{2}$, and is $1$ for all assignments in
$S_{3}$. Similarly $\mathbbm{1}(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1)$ takes
value $1$ and $0$ for all elements in $S_{2}$ and $S_{3}$, respectively.

Now we bound the magnitude of $B$,

$\displaystyle|B|=\left|\sum_{\sigma\in\\{0,1\\}^{n}}\left[\left(1-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right)\mathbbm{1}\left(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1\right)-\left(1-r(\sigma)\right)\mathbbm{1}\left(r(\sigma)<1\right)\right]P_{1}(\sigma)\right|$

For $b_{j}>0$, we have that $|\sum_{j}a_{j}b_{j}|\leq\sum_{j}|a_{j}|b_{j}$,
and thus:

$\displaystyle|B|\leq\sum_{\sigma\in\\{0,1\\}^{n}}\left|\left[\left(1-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right)\mathbbm{1}\left(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1\right)-\left(1-r(\sigma)\right)\mathbbm{1}\left(r(\sigma)<1\right)\right]\right|P_{1}(\sigma)$

We can split the summation into three terms based on the sets in which the
assignments lie. Some summands take the value $0$ in a particular set, so we
don’t include them in the term.

$\displaystyle|B|\leq$ $\displaystyle\sum_{\sigma\in
S_{1}}\mathbbm{1}\left(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1\right)\left|r(\sigma)-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right|P_{1}(\sigma)+\sum_{\sigma\in
S_{2}}\mathbbm{1}\left(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1\right)\left(1-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right)P_{1}(\sigma)$
$\displaystyle+\sum_{\sigma\in
S_{3}}\mathbbm{1}\left(r(\sigma)<1\right)\left(1-r(\sigma)\right)P_{1}(\sigma)$

Since we know that $\forall\sigma\in S_{2},r(\sigma)>1$ and $\forall\sigma\in
S_{3},\frac{P_{2}(\sigma)}{P_{1}(\sigma)}>1$, we can alter the second and
third terms of the inequality in the following way:

$\displaystyle|B|\leq$ $\displaystyle\sum_{\sigma\in
S_{1}}\mathbbm{1}\left(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1\right)\left|r(\sigma)-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right|P_{1}(\sigma)+\sum_{\sigma\in
S_{2}}\mathbbm{1}\left(\frac{P_{2}(\sigma)}{P_{1}(\sigma)}<1\right)\left|r(\sigma)-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right|P_{1}(\sigma)$
$\displaystyle+\sum_{\sigma\in
S_{3}}\mathbbm{1}\left(r(\sigma)<1\right)\left|\frac{P_{2}(\sigma)}{P_{1}(\sigma)}-r(\sigma)\right|P_{1}(\sigma)\leq\sum_{\sigma\in
S_{1}\cup S_{2}\cup
S_{3}}\left|r(\sigma)-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right|P_{1}(\sigma)$

Using our assumption of the event $\mathtt{Good}$ and Lemma 1,
$|B|\leq\sum_{\sigma\in\\{0,1\\}^{n}}\gamma/4\cdot P_{1}(\sigma)\leq\gamma/4$
Since $d_{TV}(P_{1},P_{2})-A=B$, we get $|d_{TV}(P_{1},P_{2})-A|\leq\gamma/4$.
We can now deduce that if $d_{TV}(P_{1},P_{2})\leq\varepsilon$, then
$A\leq\varepsilon+\gamma/4$ and if $d_{TV}(P_{1},P_{2})\geq\eta$, then
$A\geq\eta-\gamma/4$. ∎

##### Using $\mathsf{Teq}$ to test PCs in general.

Exact weighted model counting(WMC) is a commonly supported query on PCs. In
the language of PC queries, a WMC query is known as the marginal
($\mathsf{MAR}$) query. Conditional inference ($\mathsf{CON}$) is another well
studied PC query. Using $\mathsf{CON}$ and $\mathsf{MAR}$, one can sample from
the distribution encoded by a given PC. It is known that if a PC has the
structural properties of smoothness and decomposability, then the
$\mathsf{CON}$ and $\mathsf{MAR}$ queries can be computed tractably. For the
definitions of the above terms and further details, please refer to the survey
[9].

##  4 Evaluation

To evaluate the performance of $\mathsf{Teq}$, we implemented a prototype in
Python. The prototype uses $\mathsf{WAPS}$111https://github.com/meelgroup/WAPS
[17] as a weighted sampler to sample over the input
$\mathsf{d}$-$\mathsf{DNNF}$ circuits. The primary objective of our
experimental evaluation was to seek an answer to the following question: Is
$\mathsf{Teq}$ able to determine the closeness of a pair of probabilistic
circuits by returning $\mathsf{Accept}$ if the circuits are
$\varepsilon$-close and $\mathsf{Reject}$ if they are $\eta$-far? We test our
tool ${\mathsf{Teq}}$ in the following two settings:

  1. A.

The pair of PCs represent small randomly generated circuits and weight
functions.

  2. B.

The pair of PCs are from the set of publicly available benchmarks arising from
sampling and counting tasks.

Our experiments were conducted on a high performance compute cluster with
Intel Xeon(R) E5-2690<EMAIL_ADDRESS>CPU cores. For each benchmark, we use a
single core with a timeout of 7200 seconds.

###  4.1 Setting A - Synthetic benchmarks

##### Dataset

Our dataset for experiments conducted in setting A consisted of randomly
generated 3-$\mathsf{CNF}$s and with random literal weights. Our dataset
consisted of 3-$\mathsf{CNF}$s with $\\{14,15,16,17,18\\}$ variables. Since
the circuits are small, we validate the results by computing the actual total
variation distance using brute-force.

| $d_{TV}$ |  |
---|---|---|---
Benchmark | $\leq\epsilon$ | $\geq\eta$ | Actual | Result | Expected Result
15_3 | 0.75 | 0.94 | 0.804 | R | A/R
14_2 | 0.8 | 0.9 | 0.764 | A | A
17_4 | 0.75 | 0.9 | 0.941 | R | R
14_1 | 0.9 | 0.99 | 0.740 | A | A
18_2 | 0.75 | 0.9 | 0.918 | R | R
Table 1: Runtime performance of $\mathsf{Teq}$. We experiment with 375 random
PCs with known $d_{TV}$, and out of the 375 benchmarks we display 5 in the
table and the rest in the supplementary Section B. In the table ‘A’ represents
$\mathsf{Accept}$ and ‘R’ represents $\mathsf{Reject}$. In the last column
‘A/R’ represents that both $\mathsf{Accept}$ and $\mathsf{Reject}$ are
acceptable outputs for $\mathsf{Teq}$.

##### Results

Our tests terminated with the correct result in less than 10 seconds on all
the randomly generated PCs we experimented with. We present the empirical
results in Table 1. The first column indicates the benchmark’s name, the
second and third indicate the parameters $\varepsilon$ and $\eta$ on which we
executed $\mathsf{Teq}$. The fourth column indicates the actual $d_{TV}$
distance between the two benchmark PCs. The fifth column indicates the output
of $\mathsf{Teq}$, and the sixth indicates the expected result. The full
detailed results are presented in the appendix Section B.

###  4.2 Setting B - Real-world benchmarks

##### Dataset

We conducted experiments on a range of publicly available benchmarks arising
from sampling and counting tasks222https://zenodo.org/record/3793090. Our
dataset contained 100 $\mathsf{d}$-$\mathsf{DNNF}$ circuits with weights. We
have assigned random weights to literals wherever weights were not readily
available. For the empirical evaluation of $\mathsf{Teq}$, we needed pairs of
weighted $\mathsf{d}$-$\mathsf{DNNF}$s with known $d_{TV}$ distance. To
generate such a dataset, we first chose a circuit and a weight function, and
then we synthesized new weight functions using the technique of one variable
perturbation, described in the appendix Section B.1.

| $d_{TV}\leq\varepsilon$ | $d_{TV}\geq\eta$
---|---|---
Benchmark | Result |  $\mathsf{Teq}$(s) | Result |  $\mathsf{Teq}$(s)
or-70-10-8-UC-10 | A | 23.2 | R | 22.82
s641_15_7 | A | 33.66 | R | 33.51
or-50-5-4 | A | 414.17 | R | 408.59
ProjectService3 | A | 356.15 | R | 356.14
s713_15_7 | A | 24.86 | R | 24.41
or-100-10-2-UC-30 | A | 31.04 | R | 31.0
s1423a_3_2 | A | 153.13 | R | 152.81
s1423a_7_4 | A | 104.93 | R | 103.51
or-50-5-10 | A | 283.05 | R | 282.97
or-60-20-6-UC-20 | A | 363.32 | R | 362.8
Table 2: Runtime performance of $\mathsf{Teq}$. We experiment with 100 PCs
with known $d_{TV}$, and out of the 100 benchmarks we display 10 in the table
and the rest in the appendix B. In the table ‘A’ represents $\mathsf{Accept}$
and ‘R’ represents $\mathsf{Reject}$. The value of the closeness parameter is
$\varepsilon=0.01$ and the farness parameter is $\eta=0.2$.

##### Results

We set the closeness parameter $\varepsilon$, farness parameter $\eta$ and
confidence $\delta$ for $\mathsf{Teq}$ to be $0.01,0.2$ and $0.01$,
respectively. The chosen parameters imply that if the input pair of
probabilistic circuits are $\leq 0.01$ close in $d_{TV}$, then $\mathsf{Teq}$
returns $\mathsf{Accept}$ with probability atleast $0.99$, otherwise if the
circuits are $\geq 0.2$ far in $d_{TV}$, the algorithm returns
$\mathsf{Reject}$ with probability at least $0.99$. The number of samples
required for $\mathsf{Teq}$ (indicated by the variable $m$ as on line 2 of
Algorithm 1) depends only on $\varepsilon,\eta,\delta$ and for the values we
have chosen, we find that we require $m=294$ samples.

Our tests terminated with the correct result in less than 3600 seconds on all
the PCs we experimented with. We present the empirical results in Table 2. The
first column indicates the benchmark’s name, the second and third indicate the
result and runtime of $\mathsf{Teq}$ when presented with a pair of
$\varepsilon$-close PCs as input. Similarly, the fourth and fifth columns
indicate the result and observed runtime of $\mathsf{Teq}$ when the input PCs
are $\eta$-far . The full set of results are presented in the supplementary
Section B.

##  5 A characterization of the complexity of testing

In this section, we characterize PCs according to the complexity of closeness
and equivalence testing. We present the characterization in Table 3. The
results presented in the table can be separated into (1) hardness results, and
(2) upper bounds. The hardness results, presented in Section 5.2, are largely
derived from known complexity-theoretic results. The upper bounds, presented
in Section 5.1, are derived from a combination of established results, our
algorithm $\mathsf{Teq}$ and the exact equivalence test of Darwiche and Huang
[13](presented in supplementary Section A.1 for completeness).

###  5.1 Upper bounds

In Table 3 we label the pair of classes of PCs that admit a poly-time
closeness and equivalence test with green symbols
${\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}C}$ and
${\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}E}$
respectively. Darwiche and Huang [13] provided an equivalence test for
$\mathsf{d}$-$\mathsf{DNNF}$ s. From Theorem 1, we know that PCs that supports
the $\mathsf{Awct}$ and $\mathsf{Samp}$ queries in poly-time must also admit a
poly-time approximate equivalence test. A weighted model counting algorithms
for $\mathsf{d}$-$\mathsf{DNNF}$s was first provided by Darwiche [11], and a
weighted sampler was provided by [17]. Arenas et al. [1] provided the first
approximate counting and uniform sampling algorithm for $\mathsf{SDNNF}$s.
Using the following lemma, we show that with the use of chain formulas, the
uniform sampling and counting algorithms extend to log-linear $\mathsf{SDNNF}$
distributions as well.

######  Lemma 3.

Given a $\mathsf{SDNNF}$ formula $\varphi$ (with a v-tree ${T}$), and a weight
function $\mathtt{w}$, $\mathsf{Samp}(\varphi,\mathtt{w})$ requires polynomial
time in the size of $\varphi$.

The proof is provided in the supplementary Section A.5.

###  5.2 Hardness

In Table 3, we claim that the pairs of classes of PCs labeled with symbols
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}C}$ and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}E}$ ,
cannot be tested in poly-time for closeness equivalence, respectively. Our
claim assumes that the polynomial hierarchy (PH) does not collapse. To prove
the hardness of testing the labeled pairs, we combine previously known facts
about PCs and a few new arguments. Summarizing for brevity,

  * •

We start off by observing that PC families are in a hierarchy, with
$\mathsf{CNF}$ $\subseteq$ $\mathsf{NNF}$ and $\mathsf{DNF}$ $\subseteq$
$\mathsf{SDNNF}$ $\subseteq$ $\mathsf{DNNF}$ [14].

  * •

We then reduce the problem of satisfiability testing of $\mathsf{CNF}$s (NP-
hard) and validity testing of $\mathsf{DNF}$s (co-NP-hard) into the problem of
equivalence and closeness testing of PCs, in Propositions 1, 2 and 3. These
propositions and their proofs can be found in the supplementary Section A.5.

  * •

We then connect the existence of poly-time algorithms for equivalence to the
collapse of PH via a complexity result due to Karp and Lipton [18].

| $\mathsf{NNF}$ | $\mathsf{PI}$ | $\mathsf{DNNF}$ | $\mathsf{SDNNF}$ |  $\mathsf{d}$-$\mathsf{DNNF}$
---|---|---|---|---|---
$\mathsf{NNF}$ | $EC$ |  |  |  |
$\mathsf{PI}$ | $EC$ | $UU$ |  |  |
$\mathsf{DNNF}$ | $EC$ |  $E$$U$ |  $E$$U$ |  |
$\mathsf{SDNNF}$ | $EC$ |  $E$$U$ |  $E$$U$ |  $E$$C$ |
$\mathsf{d}$-$\mathsf{DNNF}$ | $EC$ | $UU$ |  $E$$U$ |  $E$$C$ | $EC$
Table 3:  Summary of results. C (resp. E) indicates that a poly-time closeness
(resp. equivalence) test exists. C (resp. E) indicates that a poly-time
closeness (equivalence) test exists only if PH collapses. ‘$U$’ indicates that
the existence of a poly-time test is not known. The table is best viewed in
color.

The NP-hardness of deciding the equivalence of pairs of $\mathsf{DNNF}$s and
pairs of $\mathsf{SDNNF}$s was first shown by Pipatsrisawat and Darwiche [28].
We recast their proofs in the language of distribution testing for the sake of
completeness in the supplementary Section A.5.

##  6 Conclusion and future work

In this paper, we studied the problem of closeness testing of PCs. Before our
work, poly-time algorithms were known only for the special case of equivalence
testing of PCs; and, no poly-time closeness test was known for any PC. We
provided the first such test, called $\mathsf{Teq}$, that used ideas from the
field of distribution testing to design a novel algorithm for testing the
closeness of PCs. We then implemented a prototype for $\mathsf{Teq}$, and
tested it on publicly available benchmarks to determine the runtime
performance. Experimental results demonstrate the effectiveness of
$\mathsf{Teq}$ in practice.

We also characterized PCs with respect to the complexity of deciding
equivalence and closeness. We combined known hardness results, reductions, and
our proposed algorithm $\mathsf{Teq}$ to classify pairs of PCs according to
closeness and equivalence testing complexity. Since the characterization is
incomplete, as seen in Table 3, there are questions left open regarding the
existence of tests for certain PCs, which we leave for future work.

## Broader Impact

Recent advances in probabilistic modeling techniques have led to increased
adoption of the said techniques in safety-critical domains, thus creating a
need for appropriate verification and testing methodologies. This paper seeks
to take a step in this direction and focuses on testing properties of
probabilistic models likely to find use in safety-critical domains. Since our
guarantees are probabilistic, practical adoption of such techniques still
requires careful design to handle failures.

## Acknowledgments and Disclosure of Funding

We are grateful to the anonymous reviewers of UAI 2021 and NeurIPS 2021 for
their constructive feedback that greatly improved the paper. We would also
like to thank Suwei Yang and Lawqueen Kanesh for their useful comments on the
earlier drafts of the paper. This work was supported in part by National
Research Foundation Singapore under its NRF Fellowship Programme[NRF-
NRFFAI1-2019-0004 ] and AI Singapore Programme [AISG-RP-2018-005], and NUS
ODPRT Grant [R-252-000-685-13]. The computational work for this article was
performed on resources of the National Supercomputing Centre, Singapore
(https://www.nscc.sg).

## References

  * Arenas et al. [2021] Marcelo Arenas, Luis Alberto Croquevielle, Rajesh Jayaram, and Cristian Riveros.  When is Approximate Counting for Conjunctive Queries Tractable?  In _STOC_ , 2021.
  * Aronsky and Haug [1998] Dominik Aronsky and Peter J Haug.  Diagnosing community-acquired pneumonia with a bayesian network.  In _Proceedings of the AMIA Symposium_ , 1998.
  * Cano et al. [2004] Rafael Cano, Carmen Sordo, and José M Gutiérrez.  Applications of bayesian networks in meteorology.  In _Advances in Bayesian networks_. 2004.
  * Canonne and Rubinfeld [2014] Clément Canonne and Ronitt Rubinfeld.  Testing probability distributions underlying aggregated data.  In _Automata, Languages, and Programming_ , 2014.
  * Canonne [2020] Clément L Canonne.  A survey on distribution testing: Your data is big. but is it blue?  _Theory of Computing_ , 2020.
  * Canonne et al. [2020] Clément L. Canonne, Ilias Diakonikolas, Daniel M. Kane, and Alistair Stewart.  Testing bayesian networks.  _IEEE Transactions on Information Theory_ , 2020.
  * Chakraborty and Meel [2019] Sourav Chakraborty and Kuldeep S. Meel.  On testing of uniform samplers.  In _AAAI_ , 2019.
  * Chakraborty et al. [2015] Supratik Chakraborty, Dror Fried, Kuldeep S Meel, and Moshe Y Vardi.  From weighted to unweighted model counting.  In _IJCAI_ , 2015.
  * Choi et al. [2020] YooJung Choi, Antonio Vergari, and Guy Van den Broeck.  Probabilistic circuits: A unifying framework for tractable probabilistic models.  2020\.
  * Chubarian and Turán [2020] Karine Chubarian and György Turán.  Interpretability of bayesian network classifiers: Obdd approximation and polynomial threshold functions.  In _ISAIM_ , 2020.
  * Darwiche [2001] Adnan Darwiche.  On the tractable counting of theory models and its application to truth maintenance and belief revision.  _Journal of Applied Non-Classical Logics_ , 2001.
  * Darwiche [2003] Adnan Darwiche.  A differential approach to inference in bayesian networks.  _Journal of the ACM (JACM)_ , 2003.
  * Darwiche and Huang [2002] Adnan Darwiche and Jinbo Huang.  Testing equivalence probabilistically.  In _Technical Report_ , 2002.
  * Darwiche and Marquis [2002] Adnan Darwiche and Pierre Marquis.  A knowledge compilation map.  _JAIR_ , 2002.
  * Dutta et al. [2018] Saikat Dutta, Owolabi Legunsen, Zixin Huang, and Sasa Misailovic.  Testing probabilistic programming systems.  In _Proc. of Joint Meeting on ESE and FSE_ , 2018.
  * Goodfellow et al. [2014] Ian J. Goodfellow, Jean Pouget-Abadie, Mehdi Mirza, Bing Xu, David Warde-Farley, Sherjil Ozair, Aaron Courville, and Yoshua Bengio.  Generative adversarial networks, 2014.
  * Gupta et al. [2019] Rahul Gupta, Shubham Sharma, Subhajit Roy, and Kuldeep S Meel.  Waps: Weighted and projected sampling.  In _TACAS_ , 2019.
  * Karp and Lipton [1980] Richard M. Karp and Richard J. Lipton.  Some connections between nonuniform and uniform complexity classes.  In _STOC_ , 1980.
  * Koller and Friedman [2009] Daphne Koller and Nir Friedman.  _Probabilistic graphical models: principles and techniques_.  MIT press, 2009.
  * Kulesza and Taskar [2012] Alex Kulesza and Ben Taskar.  Determinantal point processes for machine learning.  _arXiv preprint arXiv:1207.6083_ , 2012.
  * Lin et al. [2018] Zinan Lin, Ashish Khetan, Giulia Fanti, and Sewoong Oh.  Pacgan: The power of two samples in generative adversarial networks.  _NeurIPS_ , 2018.
  * Meel$ⓡ$ et al. [2020] Kuldeep S. Meel$ⓡ$, Yash Pote $ⓡ$, and Sourav Chakraborty.  On Testing of Samplers.  In _NeurIPS_ , 2020.
  * Murawski and Ouaknine [2005] Andrzej S. Murawski and Joël Ouaknine.  On probabilistic program equivalence and refinement.  In Martín Abadi and Luca de Alfaro, editors, _CONCUR_ , 2005.
  * Murphy [2012] K.P. Murphy.  _Machine Learning: A Probabilistic Perspective_.  MIT Press, 2012.
  * Oniśko et al. [2000] Agnieszka Oniśko, Marek J Druzdzel, and Hanna Wasyluk.  Extension of the hepar ii model to multiple-disorder diagnosis.  In _Intelligent Information Systems_. 2000.
  * Peharz et al. [2020a] Robert Peharz, Steven Lang, Antonio Vergari, Karl Stelzner, Alejandro Molina, Martin Trapp, Guy Van den Broeck, Kristian Kersting, and Zoubin Ghahramani.  Einsum networks: Fast and scalable learning of tractable probabilistic circuits.  In _ICML_ , 2020a.
  * Peharz et al. [2020b] Robert Peharz, Antonio Vergari, Karl Stelzner, Alejandro Molina, Xiaoting Shao, Martin Trapp, Kristian Kersting, and Zoubin Ghahramani.  Random sum-product networks: A simple and effective approach to probabilistic deep learning.  In _UAI_. PMLR, 2020b.
  * Pipatsrisawat and Darwiche [2008] Knot Pipatsrisawat and Adnan Darwiche.  New compilation languages based on structured decomposability.  In _AAAI_ , 2008.
  * Pope and Lowe [2000] Arthur R Pope and David G Lowe.  Probabilistic models of appearance for 3-d object recognition.  _International Journal of Computer Vision_ , 2000.
  * Radford et al. [2015] Alec Radford, Luke Metz, and Soumith Chintala.  Unsupervised representation learning with deep convolutional generative adversarial networks.  _arXiv preprint arXiv:1511.06434_ , 2015.
  * Rahmatallah et al. [2014] Yasir Rahmatallah, Frank Emmert-Streib, and Galina Glazko.  Gene sets net correlations analysis (gsnca): a multivariate differential coexpression test for gene sets.  _Bioinformatics_ , 2014.
  * Roth [1996] Dan Roth.  On the hardness of approximate reasoning.  _Artificial Intelligence_ , 82(1-2), 1996.
  * Städler and Mukherjee [2015] Nicolas Städler and Sach Mukherjee.  Multivariate gene-set testing based on graphical models.  _Biostatistics_ , 2015.
  * Stockmeyer [1976] Larry J. Stockmeyer.  The polynomial-time hierarchy.  _Theoretical Computer Science_ , 1976.
  * Yin et al. [2015] Weiwei Yin, Swetha Garimalla, Alberto Moreno, Mary R Galinski, and Mark P Styczynski.  A tree-like bayesian structure learning algorithm for small-sample datasets from complex biological model systems.  _BMC systems biology_ , 2015.

##  Appendix A Proofs omitted from the paper

###  A.1 A test for equivalence

For the sake of completeness we recast the $\mathsf{d}$-$\mathsf{DNNF}$
circuit equivalence test of Darwiche and Huang [13] into an equivalence test
for log-linear probability distributions.

Algorithm 2
$\mathsf{Peq}(\varphi_{1},\mathtt{w_{1}},\varphi_{2},\mathtt{w_{2}},\delta)$

1: $m\leftarrow\lceil n/\delta\rceil$

2: $\theta\sim[m]^{n}$

3: if
$\pi(\varphi_{1},\mathtt{w_{1}})(\theta)=\pi(\varphi_{2},\mathtt{w_{2}})(\theta)$
then

4: Return $\mathsf{Accept}$

5: else

6: Return $\mathsf{Reject}$

##### The algorithm:

The pseudocode for $\mathsf{Peq}$ is shown in Algorithm 2. $\mathsf{Peq}$
takes as input two satisfiable circuits $\varphi_{1},\varphi_{2}$ defined over
$n$ Boolean variables, a pair of weight functions
$\mathtt{w_{1}},\mathtt{w_{2}}$ and a tolerance parameter $\delta\in(0,1)$.
Recall that a circuit $\varphi$ and a weight function $\mathtt{w}$ together
define the probability distribution $P(\varphi,\mathtt{w})$. $\mathsf{Peq}$
returns $\mathsf{Accept}$ with confidence 1 if the two probability
distributions $P(\varphi_{1},\mathtt{w_{1}})$ and
$P(\varphi_{2},\mathtt{w_{2}})$ are equivalent, i.e.
$d_{TV}(P(\varphi_{1},\mathtt{w_{1}}),P(\varphi_{2},\mathtt{w_{2}}))=0$. If
$d_{TV}(P(\varphi_{1},\mathtt{w_{1}}),P(\varphi_{2},\mathtt{w_{2}}))>0$, then
it returns $\mathsf{Reject}$ with confidence at least $1-\delta$.

The algorithm starts by drawing a uniform random assignment $\theta$ from
$[m]^{n}$, where $m=\lceil n/\delta\rceil$. Using the procedure given in
Proposition 2 (in Section A.2), $\mathsf{Peq}$ computes the values
$\pi(\varphi_{1},\mathtt{w_{1}})(\theta)$ and
$\pi(\varphi_{2},\mathtt{w_{2}})(\theta)$, where $\pi(\varphi,\mathtt{w})$ is
the network polynomial [12]. $\pi(\varphi,\mathtt{w})$ defined as:

$\displaystyle\pi(\varphi,\mathtt{w})=\sum_{\sigma\in
R_{\varphi}}\frac{\mathtt{w}(\sigma)}{\mathtt{w}(\varphi)}\left(\prod_{x_{i}\models\sigma}x_{i}\prod_{\lnot
x_{j}\models\sigma}(1-x_{j})\right)$

The two values are then compared on line 3, and if they are equal the
algorithm returns $\mathsf{Accept}$ and otherwise returns $\mathsf{Reject}$.
The central idea of the test is that whenever the two distributions
$P(\varphi_{1},\mathtt{w_{1}})$ and $P(\varphi_{2},\mathtt{w_{2}})$ are
equivalent, the polynomials $\pi(\varphi_{1},\mathtt{w_{1}})$ and
$\pi(\varphi_{2},\mathtt{w_{2}})$ are also equivalent, however when they are
not equivalent, the polynomials disagree on atleast $1-\delta$ fraction of
assignments from the set $[m]^{n}$.

We formally claim and prove the correctness of $\mathsf{Peq}$ in Lemma 4 in
the Section A.2.

###  A.2 An analysis for Algorithm 2

In this section, we present the theoretical analysis of Algorithm 2
($\mathsf{Peq}$) and the proof of the following lemma.

######  Lemma 4.

Given two satisfiable probabilistic circuits $\varphi_{1},\varphi_{2}$ and
weight functions $\mathtt{w_{1}},\mathtt{w_{2}}$, along with confidence
parameter $\delta\in(0,1)$.

  1. A.

If $d_{TV}(P(\varphi_{1},\mathtt{w_{1}}),P(\varphi_{2},\mathtt{w_{2}}))=0$,
then
$\mathsf{Peq}(\varphi_{1},\mathtt{w_{1}},\varphi_{2},\mathtt{w_{2}},\delta)$
returns $\mathsf{Accept}$ with probability 1.

  2. B.

If $d_{TV}(P(\varphi_{1},\mathtt{w_{1}}),P(\varphi_{2},\mathtt{w_{2}}))>0$,
then
$\mathsf{Peq}(\varphi_{1},\mathtt{w_{1}},\varphi_{2},\mathtt{w_{2}},\delta)$
returns $\mathsf{Reject}$ with probability at least $(1-\delta)$.

$\mathsf{Peq}$ returns $\mathsf{Accept}$ if
$\pi(\varphi_{1},\mathtt{w_{1}})(\sigma)=\pi(\varphi_{2},\mathtt{w_{2}})(\sigma)$.
Since $P(\varphi_{1},\mathtt{w_{1}})\equiv
P(\varphi_{2},\mathtt{w_{2}})\rightarrow\pi(\varphi_{1},\mathtt{w_{1}})\equiv\pi(\varphi_{2},\mathtt{w_{2}})$,
it follows that $\mathsf{Peq}$ always returns $\mathsf{Accept}$ for two
equivalent probabilistic distributions.

For the proof of Lemma 4(B) we will first define some notation, and then we
show (in Lemma 5) that a random assignment over $[m]^{n}$ is likely to be a
witness for non-equivalence with probability $>1-\delta$. The proof
immediately follows as we know that $\mathsf{Peq}$ returns $\mathsf{Reject}$
if
$\pi(\varphi_{1},\mathtt{w_{1}})(\sigma)\not=\pi(\varphi_{2},\mathtt{w_{2}})(\sigma)$.

######  Definition 4.

$\pi|_{x_{i}=1}(\varphi,\mathtt{w})$ is a polynomial over $n-1$ variables,
obtained by setting the variable $x_{i}$ to 1. Similarly
$\pi|_{x_{i}=0}(\varphi,\mathtt{w})$ is obtained by setting the variable
$x_{i}$ to 0, thus:

$\displaystyle\pi(\varphi,\mathtt{w})=(1-x_{i})\pi|_{x_{i}=0}(\varphi,\mathtt{w})+x_{i}\pi|_{x_{i}=1}(\varphi,\mathtt{w})$

From the definition, we can immediately infer the following proposition.

######  Proposition 1.

If $\pi(\varphi_{1},\mathtt{w_{1}})\not\equiv\pi(\varphi_{2},\mathtt{w_{2}})$
then for all $x_{i}$, at least one of the following must be true:

  * •

$\pi|_{x_{i}=1}(\varphi_{1},\mathtt{w_{1}})\not=\pi|_{x_{i}=1}(\varphi_{2},\mathtt{w_{2}})$

  * •

$\pi|_{x_{i}=0}(\varphi_{1},\mathtt{w_{1}})\not=\pi|_{x_{i}=0}(\varphi_{2},\mathtt{w_{2}})$

For the proofs in this section, we will use the following notation. For a
circuit $\varphi$ defined over the variables $\\{x_{1},\ldots,x_{n}\\}$, we
define a polynomial $P(\varphi,\mathtt{w}):\\{0,1\\}^{n}\rightarrow[0,1]$:

$\displaystyle P(\varphi,\mathtt{w})=\sum_{\sigma\in
R_{\varphi}}\frac{\mathtt{w}(\sigma)}{\mathtt{w}(\varphi)}\left(\prod_{x_{i}\models\sigma}x_{i}\prod_{\lnot
x_{j}\models\sigma}(1-x_{j})\right)$

We define another polynomial $\pi(\varphi,\mathtt{w})$ which is
$P(\varphi,\mathtt{w})$ but defined from $[m]^{n}\rightarrow\mathbb{Q}$ where
$[m]=\\{1\ldots,m\\}$.

To show that the polynomial $\pi(\varphi,\mathtt{w})$ can be computed in time
polynomial in the size of the representation, we will adapt the procedure
given by [13].

######  Proposition 2.

Let $\varphi$ be a circuit over the set $X=\\{x_{1},\ldots,x_{n}\\}$ of $n$
variables , that admits poly-time WMC. Let
$\mathtt{w}:X\rightarrow\mathbb{Q}^{+}$ be a weight function and let
$\theta\in[m]^{n}$ be an assignment to the variables in $X$ and $\theta(x)$ be
the assignment to variable $x\in X$ in $\theta$. For each node $\eta$ in the
circuit, define a function ${S}()$ recursively as follows:

  * •

${S}(\eta)=\sum_{i}{S}(n_{i})$, where $\eta$ is an or-node with children
$n_{i}$.

  * •

${S}(\eta)=\prod_{i}{S}(n_{i})$, where $\eta$ is an and-node with children
$n_{i}$.

  * •

${S}(\eta)=\begin{cases}0,&\text{if }\eta\text{ is a leaf node false}\\\
1,&\text{if }\eta\text{ is a leaf node true}\\\
\mathtt{w}(x)\theta(x),&\text{if }\eta\text{ is a leaf node }x\in X\\\
(1-\mathtt{w}(x))(1-\theta(x)),&\text{if }\eta\text{ is a leaf node }\lnot
x,x\in X\\\ \end{cases}$

  * •

$\pi(\varphi,\mathtt{w})={S}(\eta)/\mathtt{w}(\varphi)$,  where $\eta$ is the
root node

We can compute the quantity $\mathtt{w}(\varphi)$ in linear time due to our
assumption of poly-time WMC, hence we can find
$\pi(\varphi,\mathtt{w})(\theta)$ in time linear in the size of the
$\mathsf{d}$-$\mathsf{DNNF}$.

######  Lemma 5.

For a random assignment $\sigma\sim[m]^{n}$,
$\Pr[\pi(\varphi_{1},{\mathtt{w_{1}}})(\sigma)\not=\pi(\varphi_{2},\mathtt{w_{2}})(\sigma)\mid
P(\varphi_{1},\mathtt{w_{1}})\not\equiv
P(\varphi_{2},\mathtt{w_{2}})]>1-\delta$

###### Proof.

For $n=1$, $\sigma$ is an assignment to a single variable $x$. The polynomial
on the single variable $x$ can be parameterised as
$\pi(\varphi,\mathtt{w})(x)=\alpha x+(1-\alpha)(1-x)$ where parameter
$\alpha=\frac{\mathtt{w(x)}}{\sum_{\theta\in R_{\varphi}}\mathtt{w(\theta)}}$.
Let polynomials
$\pi(\varphi_{1},\mathtt{w_{1}}),\pi(\varphi_{2},\mathtt{w_{2}})$ be
parameterised with $\alpha_{1},\alpha_{2}$, respectively. Our assumption that
$P(\varphi_{1},\mathtt{w_{1}})\not\equiv P(\varphi_{2},\mathtt{w_{2}})$
immediately leads to the fact that
$\pi(\varphi_{1},\mathtt{w_{1}})\not\equiv\pi(\varphi_{2},\mathtt{w_{2}})$
which in turn implies that $\alpha_{1}\not=\alpha_{2}$.

The the set of inputs $x$ for which two non-equivalent polynomials agree is
given by,

$\displaystyle\pi(\varphi_{1},\mathtt{w_{1}})(x)$
$\displaystyle=\pi(\varphi_{2},\mathtt{w_{2}})(x)$
$\displaystyle\alpha_{1}x+(1-\alpha_{1})(1-x)$
$\displaystyle=\alpha_{2}x+(1-\alpha_{2})(1-x)$ $\displaystyle
2(\alpha_{1}-\alpha_{2})x$ $\displaystyle=\alpha_{1}-\alpha_{2}$
$\displaystyle x$ $\displaystyle=1/2$

From the initial assumption we know that $x$ can only take integer values,
hence there are no inputs in the set $[m]$ for which
$\pi(\varphi_{1},\mathtt{w_{1}})(\sigma)\not=\pi(\varphi_{2},\mathtt{w_{2}})(\sigma)$.
Thus, for $n=1$, and any $\sigma$,
$\Pr[\pi(\varphi_{1},{\mathtt{w_{1}}})(\sigma)\not=\pi(\varphi_{2},\mathtt{w_{2}})(\sigma)\mid
P(\varphi_{1},\mathtt{w_{1}})\not\equiv P(\varphi_{2},\mathtt{w_{2}})]=0$

We now assume that the hypothesis holds for $n-1$ variables. Consider
polynomials
$\pi(\varphi_{1},\mathtt{w_{1}})\not\equiv\pi(\varphi_{2},\mathtt{w_{2}})$
over $n$ variables. From Prop 1 we know that at least one of the following
holds:

  * •

$\pi|_{x_{i}=1}(\varphi_{1},\mathtt{w_{1}})\not=\pi|_{x_{i}=1}(\varphi_{2},\mathtt{w_{2}})$

  * •

$\pi|_{x_{i}=0}(\varphi_{1},\mathtt{w_{1}})\not=\pi|_{x_{i}=0}(\varphi_{2},\mathtt{w_{2}})$

Without any loss of generality we assume the latter. Then we know that there
exists a set $\Sigma\subseteq[m]^{n-1},|\Sigma|\geq(m-1)^{n-1}$, such that

$\displaystyle\forall_{\sigma\in\Sigma},\pi|_{x_{n}=0}(\varphi_{1},\mathtt{w_{1}})(\sigma)\not=\pi|_{x_{n}=0}(\varphi_{2},\mathtt{w_{2}})(\sigma)$

The set of assignments $\sigma$ for which
$\pi(\varphi_{1},\mathtt{w_{1}})(\sigma)=\pi(\varphi_{2},\mathtt{w_{2}})(\sigma)$
is given by,

$\displaystyle\pi(\varphi_{1},\mathtt{w_{1}})(\sigma)$
$\displaystyle=\pi(\varphi_{2},\mathtt{w_{2}})(\sigma)$
$\displaystyle(1-x_{n})\pi|_{x_{n}=0}(\varphi_{1},\mathtt{w_{1}})(\sigma)+x_{n}\pi|_{x_{n}=1}(\varphi_{1},\mathtt{w_{1}})(\sigma)$
$\displaystyle=(1-x_{n})\pi|_{x_{n}=0}(\varphi_{2},\mathtt{w_{2}})(\sigma)+x_{n}\pi|_{x_{n}=1}(\varphi_{2},\mathtt{w_{2}})(\sigma)$
$\displaystyle
x_{n}(\pi|_{x_{n}=1}(\varphi_{1},\mathtt{w_{1}})(\sigma)-\pi|_{x_{n}=0}(\varphi_{1},\mathtt{w_{1}})(\sigma)-\pi|_{x_{n}=1}(\varphi_{2},\mathtt{w_{2}})(\sigma)+\pi|_{x_{n}=0}(\varphi_{2},\mathtt{w_{2}})(\sigma))$
$\displaystyle=\pi|_{x_{n}=0}(\varphi_{2},\mathtt{w_{2}})(\sigma)-\pi|_{x_{n}=0}(\varphi_{1},\mathtt{w_{1}})(\sigma)$

From the assumptions we know that there are at least $(m-1)^{n-1}$ assignments
$\sigma$ s.t.
$\pi|_{x_{n}=0}(\varphi_{2},\mathtt{w_{2}})(\sigma)-\pi|_{x_{n}=0}(\varphi_{1},\mathtt{w_{1}})(\sigma)\not=0$,
from which we can conclude that the RHS is non-zero. Thus for all such
$\sigma$ there can be at most one value of $x_{n}$ for which the equality
holds, which leaves $m-1$ values which $x_{n}$ cannot take. Thus there are at
least $(m-1)\times(m-1)^{n-1}=(m-1)^{n}$ assignments to $n$ variables for
which
$\pi(\varphi_{1},\mathtt{w_{1}})(\sigma)\not=\pi(\varphi_{2},\mathtt{w_{2}})(\sigma)$.

Since the total number of assignments for $n$ variables is $m^{n}$, out of
which $(m-1)^{n}$ witness the non-equivalence of the two probability
distributions, we know that for a randomly chosen assignment
$\sigma\sim[m]^{n}$, we have

$\displaystyle\Pr[\pi(\varphi_{1},{\mathtt{w_{1}}})(\sigma)\not=\pi(\varphi_{2},\mathtt{w_{2}})(\sigma)\mid
P(\varphi_{1},\mathtt{w_{1}})\not\equiv P(\varphi_{2},\mathtt{w_{2}})]$
$\displaystyle\geq\frac{(m-1)^{n}}{m^{n}}\geq\left(1-\frac{\delta}{n}\right)^{n}$
$\displaystyle>1-\delta\text{\quad(using $m$ from
Algorithm~{}\ref{alg:exactprobeq})}$

∎

###  A.3 Omitted proof from the analysis of Algorithm 1

In this subsection, we present the proof of Theorem 1(B), and Theorem 2.
Recall that we use $P_{1}$ and $P_{2}$ to refer to
$P(\varphi_{1},\mathtt{w_{1}})$ and $P(\varphi_{2},\mathtt{w_{2}})$,
respectively.

###  A.4 Proof of Lemma 1

###### Proof.

The quantity $r(\sigma)$ (line 10 from Algorithm 1) conditioned on the event
$\overline{\mathtt{Fail_{i}}}\subset\mathtt{Good}$:

$\displaystyle
r(\sigma)=\frac{\mathtt{w_{2}}(\sigma)}{\mathsf{Awct}(\sqrt{1+\gamma/4}-1,\delta/8,\varphi_{2},\mathtt{w_{2}})}\cdot\frac{\mathsf{Awct}(\sqrt{1+\gamma/4}-1,\delta/8,\varphi_{1},\mathtt{w_{1}})}{\mathtt{w_{1}}(\sigma)}$

Conditioned on the events
$\mathtt{Pass_{1}},\mathtt{Pass_{2}}\subset\mathtt{Good}$, we know that with
probability 1:

$\displaystyle\frac{\mathtt{w_{2}}(\sigma)\mathtt{w_{1}}(\varphi_{1})}{\mathtt{w_{2}}(\varphi_{2})\mathtt{w_{1}}(\sigma)}(\sqrt{1+\gamma/4})^{-2}<r(\sigma)<(\sqrt{1+\gamma/4})^{2}\frac{\mathtt{w_{2}}(\sigma)\mathtt{w_{1}}(\varphi_{1})}{\mathtt{w_{2}}(\varphi_{2})\mathtt{w_{1}}(\sigma)}$

Which gives us:
$\frac{P_{2}(\sigma)}{P_{1}(\sigma)}(1+\gamma/4)^{-1}<r(\sigma)<(1+\gamma/4)\frac{P_{2}(\sigma)}{P_{1}(\sigma)}$
and therefore,
$\left|r(\sigma)-\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\right|\leq\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\cdot\underset{0<\gamma<1}{max}\left(\gamma/4,1-\frac{1}{1+\gamma/4}\right)\leq\frac{P_{2}(\sigma)}{P_{1}(\sigma)}\cdot\gamma/4$
∎

####  A.4.1 Proof of Theorem 1(A)

###### Proof.

We assume the event $\mathtt{Good}$. Let $\sigma_{i}$ be the sample returned
by the sampler $\mathsf{Samp}$ in the $i$th iteration. If $r(\sigma_{i})>1$,
$\Gamma[i]$ takes value 0, else $\Gamma[i]=1-r(\sigma_{i})$. Thus $\Gamma[i]$
is a r.v. which takes on a value from $[0,1]$. We can write
$\Gamma[i]=\mathbbm{1}\left(r(\sigma_{i})<1\right)\left(1-r(\sigma_{i})\right)$
The expectation of $\Gamma[i]$ is:

$\displaystyle\mathbbm{E}[\Gamma[i]]=\sum_{\sigma\in\\{0,1\\}^{n}}\mathbbm{1}\left(r(\sigma)<1\right)\left(1-r(\sigma)\right)\cdot\Pr[\mathsf{Samp}(\gamma/(4\eta-2\gamma),\delta/4m,\varphi_{1},\mathtt{w_{1}})=\sigma]$
(2)

According to definition 3, and our assumption of
$\overline{\mathtt{Fail_{i}}}\subset\mathtt{Good}$, we know that with
probability 1
$\Pr[\mathsf{Samp}(\gamma/(4\eta-2\gamma),\delta/4m,\varphi_{1},\mathtt{w_{1}})=\sigma]\leq(1+\gamma/(4\eta-2\gamma))P_{1}(\sigma)$.
Thus we have,

$\displaystyle\mathbbm{E}[\Gamma[i]]$
$\displaystyle\leq\sum_{\sigma\in\\{0,1\\}^{n}}\mathbbm{1}\left(r(\sigma)<1\right)\left(1-r(\sigma)\right)\cdot(1+\gamma/(4\eta-2\gamma))P_{1}(\sigma)$

Recall that in Lemma 2, we define
$A=\sum_{\sigma\in\\{0,1\\}^{n}}\mathbbm{1}\left(r(\sigma)<1\right)\left(1-r(\sigma)\right)P_{1}(\sigma)$.
Therefore, we can simplify the above expression as:
$\mathbbm{E}[\Gamma[i]]=(1+\gamma/(4\eta-2\gamma))\cdot A$. We can then use
the assumption of $\varepsilon$-closeness and the result of Lemma 2-1 to find
a bound on the expectation,

$\displaystyle\mathbbm{E}[\Gamma[i]]$
$\displaystyle\leq\left(1+\gamma/(4\eta-2\gamma)\right)(\varepsilon+\gamma/4)\leq\varepsilon+\gamma/2$

Using the linearity of expectation we get:
$\mathbbm{E}\left[\sum_{i\in[m]}\Gamma[i]\right]<m(\varepsilon+\gamma/2)$.
$\mathsf{Teq}$ returns $\mathsf{Reject}$ when
$\sum_{i\in[m]}\Gamma[i]>m(\varepsilon+\gamma)$ on line 13. Since the
$\Gamma[i]$’s are i.i.d random variables taking values in [0, 1], we apply the
Chernoff bound to find the probability of $\mathsf{Accept}$, assuming the
event $\mathtt{Good}$:

$\displaystyle\Pr\left[\mathsf{Teq}\text{ returns
{$\mathsf{Accept}$}}~{}\bigg{|}~{}\mathtt{Good}\right]$
$\displaystyle=1-\Pr\left[\sum_{i\in[m]}\Gamma[i]>m(\varepsilon+\gamma)\right]$
$\displaystyle\geq 1-2e^{-\gamma^{2}m/2}\geq 1-\delta/2$

The value for $m$ is taken from line 2 of Algorithm 1. Using (1), we see that
the probability of $\mathsf{Teq}$ returning $\mathsf{Accept}$ is:
$\Pr[\mathsf{Teq}\text{ returns
{$\mathsf{Accept}$}}]\geq\Pr[\mathsf{Teq}\text{ returns
{$\mathsf{Accept}$}}\mid\mathtt{Good}]\Pr[\mathtt{Good}]=(1-\delta/2)(1-\delta/2)\geq
1-\delta$ ∎

####  A.4.2 Proof of Theorem 1(B)

###### Proof.

First we assume the event $\mathtt{Good}$. Then according to definition 3, we
know that with probability 1 (since we assume event
$\overline{\mathtt{Fail_{i}}}\subset\mathtt{Good}$)

$\displaystyle\Pr[\mathsf{Samp}(\gamma/(4\eta-2\gamma),\delta/4m,\varphi_{1},\mathtt{w_{1}})=\sigma]\geq\frac{P_{1}(\sigma)}{(1+\gamma/(4\eta-2\gamma))}$

Thus substituting into (2), we get

$\displaystyle\mathbbm{E}[\Gamma[i]]\geq\sum_{\sigma\in\\{0,1\\}^{n}}\mathbbm{1}\left(r(\sigma)<1\right)(1-r(\sigma))\frac{P_{1}(\sigma_{i})}{1+\gamma/(4\eta-2\gamma)}$
(3)

Then we use the $\eta$-farness assumption and Lemma 2-2

$\displaystyle\mathbbm{E}[\Gamma[i]]$
$\displaystyle\geq\frac{\eta-\gamma/4}{1+\gamma/(4\eta-2\gamma)}=\eta-\gamma/2$
(4)

The algorithm returns $\mathsf{Accept}$ when $\sum_{i\in[m]}\Gamma[i]\leq
m(\varepsilon+\gamma)$ (on line 13). Then using (4) and the linearity of
expectation.

$\displaystyle\mathbbm{E}\left[\sum_{i\in[m]}\Gamma[i]]\right]$
$\displaystyle\geq m(\eta-\gamma/2)$

Since the $\Gamma[i]$’s are i.i.d random variables taking values in [0, 1], we
apply the Chernoff bound to find the probability of $\mathsf{Reject}$, given
the assumption of the event $\mathtt{Good}$:

$\displaystyle\Pr\left[\mathsf{Teq}\text{ returns
{$\mathsf{Reject}$}}\mid\mathtt{Good}\right]$
$\displaystyle=1-\Pr\left[\sum_{i\in[m]}\Gamma[i]\leq
m(\varepsilon+\gamma)\right]$ $\displaystyle\geq
1-\Pr\left[m(\eta-\gamma/2)-\sum_{i\in[m]}\Gamma[i]\geq
m(\eta-\gamma/2-\varepsilon-\gamma)\right]$ $\displaystyle\geq
1-\Pr\left[|\sum_{i\in[m]}\Gamma[i]-m(\eta-\gamma/2)|\geq m\gamma/2\right]$
$\displaystyle\geq 1-2e^{-\gamma^{2}m/2}\geq
1-\delta/2\text{\quad(Substituting $m$ as in line \ref{line:m2})}$

Hence, the probability that Algorithm 1 returns $\mathsf{Reject}$ is

$\displaystyle\Pr[\mathsf{Teq}\text{ returns {$\mathsf{Reject}$}}]$
$\displaystyle\geq\Pr\left[\mathsf{Teq}\text{ returns
{$\mathsf{Reject}$}}\mid\mathtt{Good}\right]\Pr\left[\mathtt{Good}\right]$
$\displaystyle=(1-\delta/2)(1-\delta/2)\geq
1-\delta\quad\text{(Using~{}(\ref{line:excludebadevents}))}$

∎

####  A.4.3 Proof of Theorem 2

###### Proof.

$\mathsf{Teq}$ makes two calls to $\mathsf{Awct}$ on line 4 and 5 of Algorithm
1. According to definition 2, the runtime of the
$\mathsf{Awct}(\sqrt{1+\gamma/4}-1,\delta/8,\varphi,\mathtt{w})$ query is
$T(\sqrt{1+\gamma/4}-1,\delta/8,\varphi)=poly((\sqrt{1+\gamma/4}-1)^{-1},\log(\delta^{-1}),|\varphi|)$.

Using the identity $1+\frac{x}{2}-\frac{x^{2}}{2}\leq\sqrt{1+x}$ for $x\geq 0$
and the fact that $\gamma\in(0,1)$

$\displaystyle\frac{1}{\sqrt{1+\gamma/4}-1}\leq\frac{1}{\gamma/8-\gamma^{2}/32}<\frac{11}{\gamma}$

Hence any $poly((\sqrt{1+\gamma/4}-1)^{-1})$ algorithm also runs in
$poly(\gamma^{-1})$. Thus the $\mathsf{Awct}$ queries run in
$O(poly(\gamma^{-1},\log(\delta^{-1}),max(|\varphi_{1}|,|\varphi_{2}|)))$

$\mathsf{Teq}$ makes $m=\lceil\log(2/\delta)/2\gamma^{2}\rceil$ calls to
$\mathsf{Samp}$ on lines 7 of Algorithm 1. According to definition 3, the
runtime of the
$\mathsf{Samp}(\gamma/(4\eta-2\gamma),\delta/4m,\varphi_{1},\mathtt{w_{1}})$
query is
$T(\gamma/(4\eta-2\gamma),\delta/4m,|\varphi_{1}|)=poly((\gamma/(4\eta-2\gamma))^{-1},\log((\delta/4m)^{-1}),|\varphi_{1}|)$.
First we see that $\frac{4\eta-2\gamma}{\gamma}<\frac{4}{\gamma}$, thus the
algorithm remains in $poly(\gamma^{-1})$. We then see that
$\log(4m/\delta)=\log(4m)+\log(\delta^{-1})$. Since $\log(m)\in
poly(\log(\gamma^{-1}),\log\log(\delta^{-1}))$, we know that $\mathsf{Samp}$
queries run in
$O(poly(\gamma^{-1},\log(\delta^{-1}),max(|\varphi_{1}|,|\varphi_{2}|)))$.

Since each $\mathsf{Samp}$ call and each $\mathsf{Awct}$ call requires atmost
polynomial time in terms of $\gamma^{-1},\log(\delta^{-1})$ and
$max(|\varphi_{1}|,|\varphi_{2}|)$ we know that the algorithm itself runs in
time polynomial in $\gamma^{-1},\log(\delta^{-1})$ and
$max(|\varphi_{1}|,|\varphi_{2}|)$. ∎

###  A.5 Proofs omitted from Section 5

For the following proofs, we assume a uniform weight function.

######  Proposition 1.

If there exists a poly-time randomised algorithm for deciding the equivalence
of a pair of PCs with at least one PC in $\mathsf{CNF}$, then NP=RP.

###### Proof.

For CNFs, testing satisfiability is known to be NP-hard. Consider a CNF
$\varphi$ defined over variables $\\{x_{1},\ldots,x_{n}\\}$ and a circuit
$\psi$ s.t. $\psi\equiv\bigwedge_{i\in[n+1]}x_{i}$. Define

$\displaystyle\hat{\varphi}=(\lnot
x_{n+1}\rightarrow\varphi)\wedge(x_{n+1}\rightarrow\bigwedge_{i\in[n]}x_{i})$

We see that the size of the new CNF is $|\hat{\varphi}|\in O(|\varphi|+n)$.
$\hat{\varphi}$ has at least one satisfying assignment, specifically the
assignment $\forall_{i\in[n+1]}x_{i}=1$. We notice that
$d_{TV}(P(\hat{\varphi},\mathtt{w}),P(\psi,\mathtt{w}))=0$ if and only if
$|R_{\varphi}|=0$. Thus the existence of a poly-time randomised algorithm for
deciding whether $d_{TV}(P(\hat{\varphi},\mathtt{w}),P(\psi,\mathtt{w}))=0$
would imply NP $\subseteq$ RP and hence NP=RP. ∎

######  Proposition 2.

If there exists a poly-time randomised algorithm for deciding the closeness of
a pair of PCs with at least one PC in $\mathsf{CNF}$, then NP=RP.

###### Proof.

$d_{TV}(P(\hat{\varphi},\mathtt{w}),P(\psi,\mathtt{w}))\geq 0.5$ if and only
if $|R_{\varphi}|>0$. Assume there exists a poly-time randomised algorithm
which returns $\mathsf{Reject}$ if
$d_{TV}(P(\hat{\varphi},\mathtt{w}),P(\psi,\mathtt{w}))\geq 0.4$ and
$\mathsf{Accept}$ if
$d_{TV}(P(\hat{\varphi},\mathtt{w}),P(\psi,\mathtt{w}))\leq 0.1$ with
probability $>2/3$. Such an algorithm would imply BPP $\subseteq$ NP, and
hence NP=RP. ∎

######  Proposition 3.

If there exists a poly-time randomised algorithm for deciding the equivalence
of a pair of PCs with at least one PC in $\mathsf{DNF}$, then NP=RP.

###### Proof.

For DNFs, deciding validity is known to be co-NP-hard. Given DNF $\varphi$ and
a circuit $\psi=True$, the existence of a poly-time randomized algorithm for
checking the equivalence of $\psi$ and $\varphi$ would imply that co-NP
$\subseteq$ co-RP and hence co-NP = co-RP. ∎

Using Corollary 6.3 from [18] we see that PH collapses as a result of either
of the above implications.

From the set inclusions $\mathsf{DNF}$$\subseteq$ $\mathsf{SDNNF}$$\subseteq$
$\mathsf{DNNF}$ and $\mathsf{CNF}$$\subseteq$ $\mathsf{NNF}$, we obtain all
hardness results. From the fact that $\mathsf{d}$-$\mathsf{DNNF}$s support
weighted counting and sampling we have the existence results.

The following lemma supports our claim in table 3. See 3

###### Proof.

Here we will assume that the weights are in the dyadic form i.e. they can be
represented as the fraction $d/2^{p}$ for $d,p\in\mathbb{Z}^{+}$. Then using
the weighted to unweighted construction from [8], the problem of approximate
weighted sampling over $\mathsf{SDNNF}$ can be reduced to approximate uniform
sampling. Given a $\mathsf{SDNNF}$ $\varphi$, and a weight function
$\mathtt{w}$, we generate a $\mathsf{SDNNF}$
$\varphi_{w}\equiv\varphi\wedge\bigwedge_{i\in[n]}(\lnot x_{i}\vee
C^{1}_{i})\wedge\bigwedge_{i\in[n]}(x_{i}\vee C^{0}_{i})$. Here, $C^{0}_{i}$
is chain formula having exactly $w(\lnot x_{i})\times 2^{p}=2^{p}-d$
satisfying assignments, and $C^{1}_{i}$ is a chain formula with
$\mathtt{w}(x_{i})\times 2^{p}=d$ satisfying assignments.

The property of decomposability on the $\wedge$ nodes of $\varphi$ is
preserved as each $C_{i}$ introduces a new set of variables disjoint from the
set of variables in $\varphi$ and and also from all $C_{j}$, such that
$j\not=i$. The $\wedge$ nodes in the chain formula are also trivially
decomposable and structured as each chain formula variable appears exactly
once in the formula.

If $\sigma$ is an assignment to the set of variables of $S$ and if
$S^{\prime}\subseteq S$, then let $\sigma_{\downarrow S^{\prime}}$ denote the
projection of $\sigma$ on the variables in $S^{\prime}$. The weighted formula
$\varphi$ is defined over variable set $var(\varphi)$. The formula
$\varphi_{w}$ defined above has the property that if $\varphi(\sigma)=1$, then
$|\\{\sigma^{\prime}|\varphi_{w}(\sigma^{\prime})=1\wedge\sigma^{\prime}_{\downarrow
var(\varphi)}=\sigma\\}|/|R_{\varphi_{w}}|=\mathtt{w}(\sigma)$. Thus a uniform
distribution on $R_{\varphi_{w}}$, when projected on $var(\varphi)$ induces
the weighted distribution $P(\varphi,\mathtt{w})$. This property allows
weighted sampling and counting on $\varphi$ with the help of a uniform sampler
for the generated formula $\varphi_{w}$.∎

##  Appendix B Experimental evaluation

In this section we will first discuss the method for generating the synthetic
dataset, and then we present the extended table of results.

###  B.1 One variable perturbation

Consider two weight functions $\mathtt{w_{1}}$ and $\mathtt{w_{2}}$ that
differ only in the weight assigned to the literals $v^{0}$ and $v^{1}$. Then,
from the definition of $d_{TV}$:

$\displaystyle
d_{TV}(P(\varphi,\mathtt{w_{1}}),P(\varphi,\mathtt{w_{2}}))=\frac{1}{2}\sum_{\sigma\in\\{0,1\\}^{n}}\left|\frac{\mathtt{w_{1}}(\sigma)}{\mathtt{w_{1}}(\varphi)}-\frac{\mathtt{w_{2}}(\sigma)}{\mathtt{w_{2}}(\varphi)}\right|$

Let $S\subseteq\\{0,1\\}^{n}$ be the set of assignments for which
$\frac{\mathtt{w_{1}}(\sigma)}{\mathtt{w_{1}}(\varphi)}>\frac{\mathtt{w_{2}}(\sigma)}{\mathtt{w_{2}}(\varphi)}$.
Thus,

$\displaystyle
d_{TV}(P(\varphi,\mathtt{w_{1}}),P(\varphi,\mathtt{w_{2}}))=\sum_{\sigma\in
S}\left(\frac{\mathtt{w_{1}}(\sigma)}{\mathtt{w_{1}}(\varphi)}-\frac{\mathtt{w_{2}}(\sigma)}{\mathtt{w_{2}}(\varphi)}\right)$

Lets assume wlog that $\mathtt{w_{1}}$ assigns a larger weight to $v^{1}$ than
$\mathtt{w_{2}}$ does. Then, $S$ contains all and only those assignments that
have literal $v^{1}$, i.e. $S\equiv\varphi\wedge v^{1}$. Thus,

$\displaystyle
d_{TV}(P(\varphi,\mathtt{w_{1}}),P(\varphi,\mathtt{w_{2}}))=\frac{\mathtt{w_{1}}(\varphi\wedge
v^{1})}{\mathtt{w_{1}}(\varphi)}-\frac{\mathtt{w_{2}}(\varphi\wedge
v^{1})}{\mathtt{w_{2}}(\varphi)}$

We can rewrite $\mathtt{w_{1}}(\varphi\wedge
v^{1})=\mathtt{w_{1}^{\prime}}(\varphi)\times\mathtt{w_{1}}(v^{1})$, where
$\mathtt{w_{1}^{\prime}}$ is $\mathtt{w_{1}}$ with the weight of $v^{1}$ set
to 1. Using a similar transformation on $\mathtt{w_{2}}(\varphi\wedge v^{1})$
we get

$\displaystyle
d_{TV}(P(\varphi,\mathtt{w_{1}}),P(\varphi,\mathtt{w_{2}}))=\frac{\mathtt{w_{1}^{\prime}}(\varphi)\times\mathtt{w_{1}}(v^{1})}{\mathtt{w_{1}}(\varphi)}-\frac{\mathtt{w_{2}^{\prime}}(\varphi)\times\mathtt{w_{2}}(v^{1})}{\mathtt{w_{2}}(\varphi)}$

We know that
$\mathtt{w_{1}^{\prime}}(\varphi)=\mathtt{w_{2}^{\prime}}(\varphi)$ as
$\mathtt{w_{1}}$ and $\mathtt{w_{2}}$ differed only on the one variable
$v^{1}$.

$\displaystyle
d_{TV}(P(\varphi,\mathtt{w_{1}}),P(\varphi,\mathtt{w_{2}}))=\mathtt{w_{1}^{\prime}}(\varphi)\times\left(\frac{\mathtt{w_{1}}(v^{1})}{\mathtt{w_{1}}(\varphi)}-\frac{\mathtt{w_{2}}(v^{1})}{\mathtt{w_{2}}(\varphi)}\right)$

All quantities in the above expression are either known constants or they are
defined w.r.t the already compiled $\mathsf{d}$-$\mathsf{DNNF}$, thus
guaranteeing that
$d_{TV}(P(\varphi,\mathtt{w_{1}}),P(\varphi,\mathtt{w_{2}}))$ can be computed
in poly-time.

###  B.2 Extended table of results

The timeout for all our experiments was set to 7200 seconds.

####  B.2.1 Synthetic PCs

In the following table, the first column indicates the benchmark, the second
and the third indicate the closeness parameter $\varepsilon$ and $\eta$ used
in the test. The fourth column indicates actual $d_{TV}$ distance between the
two benchmark PCs . The fifth column indicates the test outcome and the sixth
represents the expected outcome. ‘A’ represents $\mathsf{Accept}$ and ‘R’
represents $\mathsf{Reject}$ and ‘A/R’ represents that both ‘A’ and ‘R’ are
acceptable outputs.

Table 4: The Extended Table Benchmark |  $\varepsilon$ |  $\eta$ |  Actual $d_{TV}$ |  Result |  Expected Result
---|---|---|---|---|---
14_4 |  0.9 |  0.99 |  0.773 |  A |  A
17_2 |  0.75 |  0.99 |  0.998 |  R |  R
14_2 |  0.9 |  0.99 |  0.764 |  A |  A
18_3 |  0.75 |  0.96 |  0.930 |  R |  A/R
17_4 |  0.75 |  0.99 |  0.941 |  R |  A/R
18_3 |  0.8 |  0.99 |  0.930 |  R |  A/R
17_1 |  0.8 |  0.96 |  0.874 |  R |  A/R
17_0 |  0.85 |  0.94 |  0.968 |  A |  A/R
14_2 |  0.85 |  0.94 |  0.764 |  A |  A
14_4 |  0.85 |  0.94 |  0.773 |  A |  A
15_4 |  0.9 |  0.94 |  0.941 |  R |  R
16_2 |  0.9 |  0.99 |  0.987 |  A |  A/R
14_0 |  0.75 |  0.96 |  0.771 |  A |  A/R
16_3 |  0.8 |  0.9 |  0.879 |  A |  A/R
17_2 |  0.75 |  0.96 |  0.998 |  R |  R
15_0 |  0.8 |  0.9 |  0.984 |  R |  R
18_0 |  0.75 |  0.94 |  0.994 |  R |  R
17_4 |  0.75 |  0.96 |  0.941 |  R |  A/R
18_4 |  0.75 |  0.99 |  0.907 |  R |  A/R
18_2 |  0.75 |  0.99 |  0.918 |  R |  A/R
14_1 |  0.75 |  0.99 |  0.740 |  A |  A
16_1 |  0.85 |  0.9 |  0.918 |  R |  R
17_0 |  0.85 |  0.96 |  0.968 |  A |  A/R
15_4 |  0.85 |  0.94 |  0.941 |  R |  R
17_0 |  0.8 |  0.94 |  0.968 |  A |  A/R
17_0 |  0.85 |  0.99 |  0.968 |  A |  A/R
14_0 |  0.9 |  0.94 |  0.771 |  A |  A
16_4 |  0.75 |  0.96 |  0.833 |  A |  A/R
15_1 |  0.85 |  0.96 |  0.927 |  R |  A/R
14_4 |  0.9 |  0.96 |  0.773 |  A |  A
14_3 |  0.8 |  0.96 |  0.852 |  A |  A/R
14_2 |  0.9 |  0.96 |  0.764 |  A |  A
16_4 |  0.75 |  0.9 |  0.833 |  A |  A/R
17_3 |  0.9 |  0.94 |  0.914 |  A |  A/R
15_1 |  0.85 |  0.9 |  0.927 |  R |  R
16_4 |  0.9 |  0.96 |  0.833 |  A |  A
14_3 |  0.8 |  0.94 |  0.852 |  A |  A/R
16_1 |  0.8 |  0.99 |  0.918 |  R |  A/R
16_2 |  0.85 |  0.96 |  0.987 |  A |  A/R
15_3 |  0.75 |  0.99 |  0.804 |  R |  A/R
14_3 |  0.75 |  0.94 |  0.852 |  A |  A/R
16_4 |  0.85 |  0.96 |  0.833 |  A |  A
18_0 |  0.8 |  0.9 |  0.994 |  R |  R
18_4 |  0.8 |  0.94 |  0.907 |  R |  A/R
18_4 |  0.85 |  0.99 |  0.907 |  A |  A/R
18_0 |  0.9 |  0.99 |  0.994 |  R |  R
15_1 |  0.9 |  0.99 |  0.927 |  R |  A/R
14_3 |  0.85 |  0.96 |  0.852 |  A |  A/R
16_2 |  0.75 |  0.94 |  0.987 |  R |  R
15_0 |  0.9 |  0.96 |  0.984 |  R |  R
18_4 |  0.8 |  0.96 |  0.907 |  R |  A/R
17_0 |  0.75 |  0.9 |  0.968 |  R |  R
18_1 |  0.9 |  0.96 |  0.993 |  R |  R
18_0 |  0.9 |  0.96 |  0.994 |  R |  R
17_3 |  0.8 |  0.99 |  0.914 |  A |  A/R
18_3 |  0.85 |  0.9 |  0.930 |  R |  R
17_2 |  0.85 |  0.94 |  0.998 |  R |  R
15_1 |  0.75 |  0.94 |  0.927 |  R |  A/R
14_3 |  0.75 |  0.9 |  0.852 |  R |  A/R
15_3 |  0.8 |  0.99 |  0.804 |  R |  A/R
17_3 |  0.85 |  0.94 |  0.914 |  A |  A/R
14_3 |  0.8 |  0.9 |  0.852 |  R |  A/R
17_3 |  0.75 |  0.99 |  0.914 |  R |  A/R
14_3 |  0.9 |  0.99 |  0.852 |  A |  A
17_0 |  0.75 |  0.94 |  0.968 |  R |  R
18_2 |  0.8 |  0.99 |  0.918 |  R |  A/R
17_0 |  0.8 |  0.96 |  0.968 |  A |  A/R
17_1 |  0.85 |  0.94 |  0.874 |  A |  A/R
16_3 |  0.8 |  0.94 |  0.879 |  A |  A/R
14_1 |  0.85 |  0.94 |  0.740 |  A |  A
16_3 |  0.85 |  0.99 |  0.879 |  A |  A/R
18_0 |  0.85 |  0.96 |  0.994 |  R |  R
15_3 |  0.9 |  0.94 |  0.804 |  A |  A
16_4 |  0.8 |  0.9 |  0.833 |  A |  A/R
14_1 |  0.75 |  0.96 |  0.740 |  A |  A
16_2 |  0.8 |  0.9 |  0.987 |  R |  R
17_1 |  0.75 |  0.96 |  0.874 |  R |  A/R
15_1 |  0.8 |  0.9 |  0.927 |  R |  R
15_4 |  0.8 |  0.96 |  0.941 |  R |  A/R
18_2 |  0.9 |  0.94 |  0.918 |  R |  A/R
18_4 |  0.85 |  0.94 |  0.907 |  R |  A/R
18_4 |  0.85 |  0.96 |  0.907 |  R |  A/R
16_3 |  0.9 |  0.99 |  0.879 |  A |  A
14_0 |  0.75 |  0.99 |  0.771 |  A |  A/R
16_0 |  0.85 |  0.9 |  0.954 |  R |  R
14_4 |  0.85 |  0.99 |  0.773 |  A |  A
16_1 |  0.8 |  0.9 |  0.918 |  R |  R
17_1 |  0.8 |  0.94 |  0.874 |  R |  A/R
17_1 |  0.85 |  0.99 |  0.874 |  A |  A/R
16_4 |  0.9 |  0.99 |  0.833 |  A |  A
14_1 |  0.9 |  0.94 |  0.740 |  A |  A
17_0 |  0.8 |  0.9 |  0.968 |  R |  R
14_2 |  0.75 |  0.96 |  0.764 |  A |  A/R
15_0 |  0.85 |  0.96 |  0.984 |  R |  R
14_0 |  0.8 |  0.96 |  0.771 |  A |  A
14_4 |  0.75 |  0.96 |  0.773 |  A |  A/R
16_3 |  0.75 |  0.9 |  0.879 |  R |  A/R
17_2 |  0.9 |  0.94 |  0.998 |  R |  R
15_2 |  0.85 |  0.9 |  0.905 |  A |  A/R
14_4 |  0.8 |  0.94 |  0.773 |  A |  A
14_2 |  0.8 |  0.94 |  0.764 |  A |  A
16_0 |  0.8 |  0.99 |  0.954 |  R |  A/R
17_2 |  0.85 |  0.9 |  0.998 |  R |  R
16_3 |  0.85 |  0.96 |  0.879 |  A |  A/R
14_2 |  0.75 |  0.94 |  0.764 |  A |  A/R
18_1 |  0.8 |  0.94 |  0.993 |  R |  R
18_1 |  0.85 |  0.99 |  0.993 |  R |  R
18_1 |  0.9 |  0.99 |  0.993 |  R |  R
16_4 |  0.75 |  0.99 |  0.833 |  A |  A/R
15_0 |  0.9 |  0.99 |  0.984 |  R |  A/R
15_1 |  0.9 |  0.96 |  0.927 |  R |  A/R
16_0 |  0.9 |  0.94 |  0.954 |  A |  A/R
17_1 |  0.75 |  0.9 |  0.874 |  R |  A/R
15_0 |  0.8 |  0.94 |  0.984 |  R |  R
17_4 |  0.8 |  0.99 |  0.941 |  R |  A/R
18_2 |  0.85 |  0.9 |  0.918 |  R |  R
14_2 |  0.75 |  0.9 |  0.764 |  A |  A/R
15_0 |  0.8 |  0.99 |  0.984 |  R |  A/R
14_2 |  0.8 |  0.9 |  0.764 |  A |  A
14_4 |  0.8 |  0.9 |  0.773 |  A |  A
14_1 |  0.85 |  0.9 |  0.740 |  A |  A
17_0 |  0.75 |  0.99 |  0.968 |  A |  A/R
14_0 |  0.85 |  0.9 |  0.771 |  A |  A
17_1 |  0.75 |  0.94 |  0.874 |  R |  A/R
18_1 |  0.85 |  0.94 |  0.993 |  R |  R
18_1 |  0.8 |  0.99 |  0.993 |  R |  R
18_1 |  0.75 |  0.9 |  0.993 |  R |  R
17_3 |  0.8 |  0.96 |  0.914 |  R |  A/R
18_3 |  0.9 |  0.96 |  0.930 |  R |  A/R
16_2 |  0.8 |  0.94 |  0.987 |  A |  A/R
14_0 |  0.85 |  0.94 |  0.771 |  A |  A
16_2 |  0.85 |  0.99 |  0.987 |  A |  A/R
16_4 |  0.8 |  0.94 |  0.833 |  A |  A/R
18_1 |  0.85 |  0.96 |  0.993 |  R |  R
16_4 |  0.85 |  0.99 |  0.833 |  A |  A
15_2 |  0.9 |  0.94 |  0.905 |  A |  A/R
15_0 |  0.75 |  0.9 |  0.984 |  R |  R
16_0 |  0.9 |  0.99 |  0.954 |  A |  A/R
15_4 |  0.8 |  0.9 |  0.941 |  R |  R
17_0 |  0.75 |  0.96 |  0.968 |  R |  R
15_3 |  0.8 |  0.96 |  0.804 |  R |  A/R
18_3 |  0.9 |  0.94 |  0.930 |  R |  A/R
18_3 |  0.85 |  0.94 |  0.930 |  R |  A/R
16_0 |  0.8 |  0.96 |  0.954 |  A |  A/R
17_4 |  0.85 |  0.96 |  0.941 |  R |  A/R
14_3 |  0.75 |  0.99 |  0.852 |  A |  A/R
17_2 |  0.85 |  0.96 |  0.998 |  R |  R
17_4 |  0.8 |  0.94 |  0.941 |  R |  R
16_2 |  0.8 |  0.96 |  0.987 |  A |  A/R
17_4 |  0.85 |  0.99 |  0.941 |  R |  A/R
16_3 |  0.8 |  0.96 |  0.879 |  A |  A/R
17_1 |  0.8 |  0.9 |  0.874 |  R |  A/R
16_2 |  0.75 |  0.96 |  0.987 |  R |  R
15_3 |  0.85 |  0.96 |  0.804 |  A |  A
17_2 |  0.8 |  0.94 |  0.998 |  R |  R
14_1 |  0.8 |  0.96 |  0.740 |  A |  A
14_0 |  0.85 |  0.99 |  0.771 |  A |  A
16_2 |  0.75 |  0.9 |  0.987 |  R |  R
15_2 |  0.85 |  0.94 |  0.905 |  A |  A/R
14_3 |  0.85 |  0.99 |  0.852 |  A |  A/R
15_3 |  0.85 |  0.9 |  0.804 |  R |  A/R
14_2 |  0.85 |  0.99 |  0.764 |  A |  A
16_3 |  0.8 |  0.99 |  0.879 |  A |  A/R
17_3 |  0.85 |  0.9 |  0.914 |  A |  A/R
16_0 |  0.85 |  0.96 |  0.954 |  A |  A/R
14_1 |  0.75 |  0.94 |  0.740 |  A |  A
18_4 |  0.8 |  0.9 |  0.907 |  R |  R
18_0 |  0.8 |  0.94 |  0.994 |  R |  R
14_3 |  0.8 |  0.99 |  0.852 |  A |  A/R
18_0 |  0.85 |  0.99 |  0.994 |  R |  R
18_2 |  0.9 |  0.99 |  0.918 |  R |  A/R
16_3 |  0.75 |  0.99 |  0.879 |  A |  A/R
15_3 |  0.9 |  0.99 |  0.804 |  A |  A
16_4 |  0.75 |  0.94 |  0.833 |  A |  A/R
15_2 |  0.9 |  0.96 |  0.905 |  A |  A/R
16_1 |  0.9 |  0.94 |  0.918 |  R |  A/R
18_2 |  0.8 |  0.96 |  0.918 |  R |  A/R
17_2 |  0.9 |  0.96 |  0.998 |  R |  R
15_1 |  0.8 |  0.94 |  0.927 |  R |  A/R
17_3 |  0.9 |  0.99 |  0.914 |  A |  A/R
15_1 |  0.75 |  0.96 |  0.927 |  R |  A/R
15_1 |  0.8 |  0.99 |  0.927 |  R |  A/R
14_1 |  0.8 |  0.9 |  0.740 |  A |  A
17_4 |  0.75 |  0.94 |  0.941 |  R |  R
18_0 |  0.75 |  0.96 |  0.994 |  R |  R
17_1 |  0.75 |  0.99 |  0.874 |  R |  A/R
17_2 |  0.75 |  0.94 |  0.998 |  R |  R
18_0 |  0.8 |  0.99 |  0.994 |  R |  R
18_0 |  0.75 |  0.9 |  0.994 |  R |  R
17_2 |  0.8 |  0.96 |  0.998 |  R |  R
18_2 |  0.9 |  0.96 |  0.918 |  R |  A/R
16_1 |  0.8 |  0.94 |  0.918 |  R |  A/R
16_1 |  0.85 |  0.99 |  0.918 |  R |  A/R
18_2 |  0.85 |  0.96 |  0.918 |  R |  A/R
15_1 |  0.9 |  0.94 |  0.927 |  R |  A/R
15_1 |  0.75 |  0.9 |  0.927 |  R |  R
16_1 |  0.9 |  0.99 |  0.918 |  R |  A/R
14_3 |  0.75 |  0.96 |  0.852 |  A |  A/R
18_3 |  0.75 |  0.94 |  0.930 |  R |  A/R
15_2 |  0.8 |  0.96 |  0.905 |  A |  A/R
18_0 |  0.9 |  0.94 |  0.994 |  R |  R
18_1 |  0.75 |  0.99 |  0.993 |  R |  R
18_2 |  0.85 |  0.94 |  0.918 |  R |  A/R
17_3 |  0.85 |  0.96 |  0.914 |  A |  A/R
14_2 |  0.75 |  0.99 |  0.764 |  A |  A/R
15_3 |  0.85 |  0.94 |  0.804 |  A |  A
17_2 |  0.8 |  0.9 |  0.998 |  R |  R
16_3 |  0.75 |  0.96 |  0.879 |  A |  A/R
14_2 |  0.85 |  0.9 |  0.764 |  A |  A
15_2 |  0.85 |  0.96 |  0.905 |  A |  A/R
14_1 |  0.9 |  0.96 |  0.740 |  A |  A
16_1 |  0.75 |  0.9 |  0.918 |  R |  R
17_4 |  0.9 |  0.94 |  0.941 |  R |  R
15_4 |  0.85 |  0.9 |  0.941 |  R |  R
16_4 |  0.8 |  0.99 |  0.833 |  A |  A/R
15_0 |  0.75 |  0.99 |  0.984 |  R |  A/R
15_0 |  0.85 |  0.9 |  0.984 |  R |  R
16_2 |  0.8 |  0.99 |  0.987 |  A |  A/R
17_0 |  0.85 |  0.9 |  0.968 |  A |  A/R
16_1 |  0.85 |  0.96 |  0.918 |  R |  A/R
14_0 |  0.75 |  0.94 |  0.771 |  A |  A/R
16_2 |  0.9 |  0.96 |  0.987 |  A |  A/R
18_3 |  0.8 |  0.9 |  0.930 |  R |  R
18_3 |  0.8 |  0.94 |  0.930 |  R |  A/R
14_2 |  0.8 |  0.99 |  0.764 |  A |  A
16_1 |  0.9 |  0.96 |  0.918 |  R |  A/R
18_3 |  0.85 |  0.99 |  0.930 |  R |  A/R
14_4 |  0.8 |  0.99 |  0.773 |  A |  A
16_0 |  0.9 |  0.96 |  0.954 |  A |  A/R
18_3 |  0.9 |  0.99 |  0.930 |  R |  A/R
16_2 |  0.75 |  0.99 |  0.987 |  A |  A/R
14_0 |  0.85 |  0.96 |  0.771 |  A |  A
15_2 |  0.9 |  0.99 |  0.905 |  A |  A/R
16_1 |  0.75 |  0.94 |  0.918 |  R |  A/R
16_4 |  0.9 |  0.94 |  0.833 |  A |  A
15_3 |  0.9 |  0.96 |  0.804 |  A |  A
16_2 |  0.9 |  0.94 |  0.987 |  A |  A/R
18_3 |  0.8 |  0.96 |  0.930 |  R |  A/R
17_3 |  0.9 |  0.96 |  0.914 |  A |  A/R
15_2 |  0.8 |  0.94 |  0.905 |  A |  A/R
17_0 |  0.8 |  0.99 |  0.968 |  A |  A/R
15_2 |  0.75 |  0.94 |  0.905 |  R |  A/R
18_4 |  0.85 |  0.9 |  0.907 |  R |  R
15_4 |  0.8 |  0.99 |  0.941 |  R |  A/R
15_4 |  0.75 |  0.94 |  0.941 |  R |  R
14_4 |  0.75 |  0.9 |  0.773 |  A |  A/R
14_0 |  0.8 |  0.9 |  0.771 |  A |  A
14_0 |  0.9 |  0.99 |  0.771 |  A |  A
18_1 |  0.75 |  0.96 |  0.993 |  R |  R
17_3 |  0.75 |  0.94 |  0.914 |  R |  A/R
18_3 |  0.75 |  0.9 |  0.930 |  R |  R
17_4 |  0.85 |  0.94 |  0.941 |  R |  R
16_0 |  0.8 |  0.94 |  0.954 |  A |  A/R
15_0 |  0.85 |  0.99 |  0.984 |  R |  A/R
16_0 |  0.85 |  0.99 |  0.954 |  A |  A/R
15_4 |  0.75 |  0.9 |  0.941 |  R |  R
15_1 |  0.85 |  0.99 |  0.927 |  R |  A/R
18_3 |  0.85 |  0.96 |  0.930 |  R |  A/R
15_0 |  0.9 |  0.94 |  0.984 |  R |  R
15_2 |  0.75 |  0.9 |  0.905 |  R |  R
15_2 |  0.85 |  0.99 |  0.905 |  A |  A/R
15_2 |  0.8 |  0.9 |  0.905 |  A |  A/R
15_3 |  0.85 |  0.99 |  0.804 |  A |  A
18_2 |  0.75 |  0.94 |  0.918 |  R |  A/R
18_4 |  0.75 |  0.94 |  0.907 |  R |  A/R
15_1 |  0.8 |  0.96 |  0.927 |  R |  A/R
18_1 |  0.9 |  0.94 |  0.993 |  R |  R
18_0 |  0.75 |  0.99 |  0.994 |  R |  R
14_3 |  0.85 |  0.9 |  0.852 |  A |  A/R
16_3 |  0.85 |  0.9 |  0.879 |  A |  A/R
16_1 |  0.8 |  0.96 |  0.918 |  R |  A/R
14_1 |  0.85 |  0.99 |  0.740 |  A |  A
15_0 |  0.85 |  0.94 |  0.984 |  R |  R
17_2 |  0.85 |  0.99 |  0.998 |  R |  R
14_2 |  0.9 |  0.94 |  0.764 |  A |  A
14_4 |  0.9 |  0.94 |  0.773 |  A |  A
17_3 |  0.8 |  0.9 |  0.914 |  R |  R
16_0 |  0.75 |  0.96 |  0.954 |  R |  A/R
14_0 |  0.9 |  0.96 |  0.771 |  A |  A
17_1 |  0.9 |  0.94 |  0.874 |  A |  A
16_0 |  0.75 |  0.9 |  0.954 |  R |  R
14_1 |  0.8 |  0.94 |  0.740 |  A |  A
15_1 |  0.75 |  0.99 |  0.927 |  R |  A/R
17_1 |  0.85 |  0.9 |  0.874 |  R |  A/R
18_2 |  0.8 |  0.9 |  0.918 |  R |  R
18_2 |  0.8 |  0.94 |  0.918 |  R |  A/R
14_1 |  0.8 |  0.99 |  0.740 |  A |  A
18_2 |  0.85 |  0.99 |  0.918 |  R |  A/R
18_4 |  0.9 |  0.99 |  0.907 |  A |  A/R
16_1 |  0.75 |  0.99 |  0.918 |  R |  A/R
14_1 |  0.85 |  0.96 |  0.740 |  A |  A
16_0 |  0.75 |  0.94 |  0.954 |  R |  R
15_4 |  0.9 |  0.96 |  0.941 |  R |  A/R
17_2 |  0.75 |  0.9 |  0.998 |  R |  R
16_3 |  0.9 |  0.94 |  0.879 |  A |  A
18_0 |  0.8 |  0.96 |  0.994 |  R |  R
17_4 |  0.75 |  0.9 |  0.941 |  R |  R
15_3 |  0.8 |  0.94 |  0.804 |  R |  A/R
17_1 |  0.8 |  0.99 |  0.874 |  R |  A/R
18_1 |  0.85 |  0.9 |  0.993 |  R |  R
15_3 |  0.75 |  0.94 |  0.804 |  R |  A/R
14_1 |  0.75 |  0.9 |  0.740 |  A |  A
17_1 |  0.9 |  0.99 |  0.874 |  A |  A
15_3 |  0.75 |  0.96 |  0.804 |  R |  A/R
18_4 |  0.75 |  0.96 |  0.907 |  R |  A/R
14_1 |  0.9 |  0.99 |  0.740 |  A |  A
18_2 |  0.75 |  0.96 |  0.918 |  R |  A/R
18_4 |  0.8 |  0.99 |  0.907 |  R |  A/R
18_4 |  0.75 |  0.9 |  0.907 |  R |  R
18_2 |  0.75 |  0.9 |  0.918 |  R |  R
17_4 |  0.8 |  0.96 |  0.941 |  R |  A/R
14_3 |  0.85 |  0.94 |  0.852 |  A |  A/R
18_4 |  0.9 |  0.96 |  0.907 |  A |  A/R
17_3 |  0.75 |  0.9 |  0.914 |  R |  R
17_4 |  0.9 |  0.96 |  0.941 |  R |  A/R
15_3 |  0.75 |  0.9 |  0.804 |  R |  A/R
16_0 |  0.8 |  0.9 |  0.954 |  R |  R
17_3 |  0.75 |  0.96 |  0.914 |  R |  A/R
15_3 |  0.8 |  0.9 |  0.804 |  R |  A/R
18_1 |  0.75 |  0.94 |  0.993 |  R |  R
16_1 |  0.85 |  0.94 |  0.918 |  R |  A/R
16_3 |  0.85 |  0.94 |  0.879 |  A |  A/R
18_4 |  0.9 |  0.94 |  0.907 |  A |  A/R
15_0 |  0.8 |  0.96 |  0.984 |  R |  R
16_0 |  0.85 |  0.94 |  0.954 |  A |  A/R
14_4 |  0.85 |  0.9 |  0.773 |  A |  A
18_3 |  0.75 |  0.99 |  0.930 |  R |  A/R
17_0 |  0.9 |  0.96 |  0.968 |  A |  A/R
18_0 |  0.85 |  0.94 |  0.994 |  R |  R
17_1 |  0.9 |  0.96 |  0.874 |  A |  A
16_4 |  0.8 |  0.96 |  0.833 |  A |  A/R
16_2 |  0.85 |  0.9 |  0.987 |  A |  A/R
17_1 |  0.85 |  0.96 |  0.874 |  A |  A/R
14_4 |  0.75 |  0.99 |  0.773 |  A |  A/R
16_4 |  0.85 |  0.9 |  0.833 |  A |  A
17_3 |  0.8 |  0.94 |  0.914 |  R |  A/R
15_1 |  0.85 |  0.94 |  0.927 |  R |  A/R
17_3 |  0.85 |  0.99 |  0.914 |  A |  A/R
14_3 |  0.9 |  0.94 |  0.852 |  A |  A
17_4 |  0.8 |  0.9 |  0.941 |  R |  R
16_1 |  0.75 |  0.96 |  0.918 |  R |  A/R
15_4 |  0.85 |  0.96 |  0.941 |  R |  A/R
14_2 |  0.8 |  0.96 |  0.764 |  A |  A
14_3 |  0.9 |  0.96 |  0.852 |  A |  A
17_0 |  0.9 |  0.94 |  0.968 |  A |  A/R
14_4 |  0.8 |  0.96 |  0.773 |  A |  A
16_3 |  0.9 |  0.96 |  0.879 |  A |  A
15_4 |  0.75 |  0.99 |  0.941 |  R |  A/R
14_0 |  0.8 |  0.94 |  0.771 |  A |  A
17_4 |  0.85 |  0.9 |  0.941 |  R |  R
15_2 |  0.75 |  0.99 |  0.905 |  A |  A/R
14_4 |  0.75 |  0.94 |  0.773 |  A |  A/R
17_4 |  0.9 |  0.99 |  0.941 |  A |  A/R
18_1 |  0.8 |  0.9 |  0.993 |  R |  R
15_4 |  0.85 |  0.99 |  0.941 |  R |  A/R
14_0 |  0.8 |  0.99 |  0.771 |  A |  A
17_2 |  0.9 |  0.99 |  0.998 |  R |  R
14_0 |  0.75 |  0.9 |  0.771 |  A |  A/R
14_4 |  0.85 |  0.96 |  0.773 |  A |  A
16_0 |  0.75 |  0.99 |  0.954 |  R |  A/R
14_2 |  0.85 |  0.96 |  0.764 |  A |  A
15_4 |  0.9 |  0.99 |  0.941 |  A |  A/R
16_3 |  0.75 |  0.94 |  0.879 |  R |  A/R
16_4 |  0.85 |  0.94 |  0.833 |  A |  A
18_1 |  0.8 |  0.96 |  0.993 |  R |  R
15_0 |  0.75 |  0.96 |  0.984 |  R |  R
16_2 |  0.85 |  0.94 |  0.987 |  A |  A/R
15_4 |  0.8 |  0.94 |  0.941 |  R |  R
17_2 |  0.8 |  0.99 |  0.998 |  R |  R
18_0 |  0.85 |  0.9 |  0.994 |  R |  R
15_0 |  0.75 |  0.94 |  0.984 |  R |  R
15_4 |  0.75 |  0.96 |  0.941 |  R |  A/R
17_0 |  0.9 |  0.99 |  0.968 |  A |  A/R
15_2 |  0.8 |  0.99 |  0.905 |  A |  A/R
15_2 |  0.75 |  0.96 |  0.905 |  R |  A/R

####  B.2.2 Real-world PCs

In the following table, the first column indicates the benchmark, the second
indicates the time required for the test, and the third column indicates the
test outcome. ‘A’ represents $\mathsf{Accept}$ and ‘R’ represents
$\mathsf{Reject}$.

Table 5: The Extended Table Benchmark |  $\mathsf{Teq}$(s) |  Result
---|---|---
or-70-10-8-UC-10_0 |  23.2 |  A
or-70-10-8-UC-10_1 |  22.72 |  R
or-70-10-8-UC-10_2 |  22.92 |  R
or-70-10-8-UC-10_3 |  22.87 |  R
or-70-10-8-UC-10_4 |  22.78 |  R
or-70-10-8-UC-10_5 |  23.06 |  R
or-70-10-8-UC-10_6 |  22.99 |  R
or-70-10-8-UC-10_7 |  22.93 |  R
or-70-10-8-UC-10_8 |  22.82 |  R
or-70-10-8-UC-10_9 |  22.82 |  R
s641_15_7_0 |  33.66 |  A
s641_15_7_1 |  33.4 |  R
s641_15_7_2 |  33.45 |  R
s641_15_7_3 |  33.32 |  R
s641_15_7_4 |  33.51 |  R
s641_15_7_5 |  33.21 |  R
s641_15_7_6 |  33.46 |  R
s641_15_7_7 |  33.23 |  R
s641_15_7_8 |  33.61 |  R
s641_15_7_9 |  33.51 |  R
or-50-5-4_0 |  414.17 |  A
or-50-5-4_1 |  414.84 |  R
or-50-5-4_2 |  410.16 |  R
or-50-5-4_3 |  414.15 |  R
or-50-5-4_4 |  410.07 |  R
or-50-5-4_5 |  412.27 |  R
or-50-5-4_6 |  414.77 |  R
or-50-5-4_7 |  415.19 |  R
or-50-5-4_8 |  416.84 |  R
or-50-5-4_9 |  408.59 |  R
ProjectService3.sk_12_55_0 |  356.58 |  A
ProjectService3.sk_12_55_1 |  353.77 |  R
ProjectService3.sk_12_55_2 |  355.93 |  R
ProjectService3.sk_12_55_3 |  356.11 |  R
ProjectService3.sk_12_55_4 |  356.15 |  A
ProjectService3.sk_12_55_5 |  355.64 |  R
ProjectService3.sk_12_55_6 |  357.89 |  R
ProjectService3.sk_12_55_7 |  356.69 |  R
ProjectService3.sk_12_55_8 |  353.36 |  R
ProjectService3.sk_12_55_9 |  356.14 |  R
s713_15_7_0 |  24.56 |  R
s713_15_7_1 |  24.68 |  R
s713_15_7_2 |  24.28 |  R
s713_15_7_3 |  24.47 |  R
s713_15_7_4 |  24.65 |  R
s713_15_7_5 |  24.32 |  R
s713_15_7_6 |  24.4 |  R
s713_15_7_7 |  24.39 |  R
s713_15_7_8 |  24.86 |  A
s713_15_7_9 |  24.41 |  R
or-100-10-2-UC-30_0 |  31.11 |  R
or-100-10-2-UC-30_1 |  31.16 |  R
or-100-10-2-UC-30_2 |  31.04 |  R
or-100-10-2-UC-30_3 |  31.13 |  R
or-100-10-2-UC-30_4 |  31.14 |  R
or-100-10-2-UC-30_5 |  31.04 |  A
or-100-10-2-UC-30_6 |  31.03 |  R
or-100-10-2-UC-30_7 |  31.13 |  R
or-100-10-2-UC-30_8 |  31.17 |  R
or-100-10-2-UC-30_9 |  31.0 |  R
s1423a_3_2_0 |  153.8 |  R
s1423a_3_2_1 |  152.37 |  R
s1423a_3_2_2 |  152.01 |  R
s1423a_3_2_3 |  150.96 |  R
s1423a_3_2_4 |  152.64 |  R
s1423a_3_2_5 |  153.13 |  A
s1423a_3_2_6 |  151.52 |  R
s1423a_3_2_7 |  152.53 |  R
s1423a_3_2_8 |  152.4 |  R
s1423a_3_2_9 |  152.81 |  R
s1423a_7_4_0 |  104.28 |  R
s1423a_7_4_1 |  103.4 |  R
s1423a_7_4_2 |  103.82 |  R
s1423a_7_4_3 |  104.18 |  R
s1423a_7_4_4 |  103.95 |  R
s1423a_7_4_5 |  103.59 |  R
s1423a_7_4_6 |  104.31 |  R
s1423a_7_4_7 |  104.93 |  R
s1423a_7_4_8 |  104.93 |  A
s1423a_7_4_9 |  103.51 |  R
or-50-5-10_0 |  282.09 |  R
or-50-5-10_1 |  282.49 |  R
or-50-5-10_2 |  279.63 |  R
or-50-5-10_3 |  281.8 |  R
or-50-5-10_4 |  280.69 |  R
or-50-5-10_5 |  279.91 |  R
or-50-5-10_6 |  283.05 |  A
or-50-5-10_7 |  282.69 |  R
or-50-5-10_8 |  279.65 |  R
or-50-5-10_9 |  282.97 |  R
or-60-20-6-UC-20_0 |  359.89 |  R
or-60-20-6-UC-20_1 |  362.3 |  R
or-60-20-6-UC-20_2 |  363.1 |  R
or-60-20-6-UC-20_3 |  363.11 |  R
or-60-20-6-UC-20_4 |  362.76 |  R
or-60-20-6-UC-20_5 |  358.76 |  R
or-60-20-6-UC-20_6 |  363.32 |  A
or-60-20-6-UC-20_7 |  358.41 |  R
or-60-20-6-UC-20_8 |  358.8 |  R
or-60-20-6-UC-20_9 |  362.8 |  R