=Paper=
{{Paper
|id=Vol-2157/paper4
|storemode=property
|title=A New Probabilistic Algorithm for Approximate Model Counting and Extensions for Numeric Domains
|pdfUrl=https://ceur-ws.org/Vol-2157/paper4.pdf
|volume=Vol-2157
|authors=Cunjing Ge,Feifei Ma,Tian Liu,Jian Zhang,Xutong Ma
|dblpUrl=https://dblp.org/rec/conf/cade/GeML0M18
}}
==A New Probabilistic Algorithm for Approximate Model Counting and Extensions for Numeric Domains==
https://ceur-ws.org/Vol-2157/paper4.pdf
A New Probabilistic Algorithm for Approximate Model
Counting and Extensions for Numeric Domains ?
Cunjing Ge1,3 , Feifei Ma1,2,3 ( ), Tian Liu4 , Jian Zhang1,3 , and Xutong Ma3,5
1
State Key Laboratory of Computer Science,
Institute of Software, Chinese Academy of Sciences
{gecj, maff, zj}@ios.ac.cn
2
Laboratory of Parallel Software and Computational Science,
Institute of Software, Chinese Academy of Sciences
3
University of Chinese Academy of Sciences
4
School of Electronics Engineering and Computer Science, Peking University
5
Technology Center of Software Engineering,
Institute of Software, Chinese Academy of Sciences
Abstract. Constrained counting is important in domains ranging from artificial
intelligence to software analysis. There are already a few approaches for count-
ing models over various types of constraints. Recently, hashing-based approach-
es achieve success but still rely on solution enumeration. In the IJCAR version,
a probabilistic approximate model counter is proposed, which is also a hashing-
based universal framework, but with only satisfiability queries. A dynamic stop-
ping criteria, for the algorithm, is presented, which has not been studied yet in
previous works of hashing-based approaches. Although the algorithm lacks the-
oretical guarantee, it works well in practice. In this paper, we further extend our
approach to SMT(LIA) formulas with a new encoding technique.
1 Introduction
Constrained counting, the problem of counting the number of solutions for a set of
constraints, is important in theoretical computer science and artificial intelligence. It-
s interesting applications in several fields include program analysis [25, 18, 19, 15, 27,
16], probabilistic inference [28, 11], planning [13] and privacy/confidentiality verifica-
tion [17]. Constrained counting for propositional formulas is also called model count-
ing, to which probabilistic inference is easily reducible. However, model counting is
a canonical #P-complete problem, even for polynomial-time solvable problems like 2-
SAT [33], thus it presents fascinating challenges for both theoreticians and practitioners.
There are already a few approaches for counting solutions over propositional logic
formulas and SMT(BV) formulas. Recently, hashing-based approximate counting achi-
eves both strong theoretical guarantees and good scalability [26]. The use of universal
?
This work has been supported by the National 973 Program of China under Grant
2014CB340701, Key Research Program of Frontier Sciences, Chinese Academy of Sciences
(CAS) under Grant QYZDJ-SSW-JSC036, and the National Natural Science Foundation of
China under Grant 61100064. Feifei Ma is also supported by the Youth Innovation Promotion
Association, CAS.
2 Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, and Xutong Ma
hash functions in counting problems began in [30, 32], but the resulting algorithm scaled
poorly in practice. A scalable approximate counter ApproxMC in [9] scales to large
problem instances, while preserving rigorous approximation guarantees. ApproxMC
has been extended to finite-domain discrete integration, with applications to probabilis-
tic inference [14, 6, 3]. It was improved by designing efficient universal hash functions
[22, 7] and reducing the use of NP-oracle calls from linear to logarithmic [10].
The basic idea in ApproxMC is to estimate the model count by randomly and it-
eratively cutting the whole space down to a small “enough” cell, using hash functions,
and sampling it. The total model count is estimated by a multiplication of the number
of solutions in this cell and the ratio of the whole space to the small cell. To determine
the size of the small cell, which is essentially a small-scale model counting problem
with the model counts bounded by some thresholds, a model enumeration in the cell
is adopted. In previous works, the enumeration query was handled by transforming it
into a series of satisfiability queries, which is much more time-consuming than a single
satisfiability query. An algorithm called MBound [20] only invokes satisfiability query
once for each cut. Its model count is determined with high precision by the number of
cuts down to the boundary of being unsatisfiable. However, this property is not strong
enough to give rigorous guarantees, and MBound only returns an approximation of
upper or lower bound of the model count.
In the IJCAR version, a hashing-based approximate counting algorithm, with only
satisfiability query, is proposed. Dynamic stopping criterion for the algorithm to termi-
nate, once meeting the criterion of accuracy, is presented, which has not been proposed
yet in previous works of hashing-based approaches. Theoretical insights over the effi-
ciency of a prevalent heuristic strategy called leap-frogging are also provided. Proto-
type tools for propositional logic formulas, SMT(BV) formulas are implemented. An
extensive evaluation on a suite of benchmarks demonstrates that (i) the approach signifi-
cantly outperforms the state-of-the-art approximate model counters, including a counter
designed for SMT(BV) formulas, and (ii) the dynamic stopping criterion is promising.
In this paper, we further present a new technique to encode XOR-based hash func-
tion over numeric domains. In addition, our approach is a general framework. Thus we
managed to extend it to numeric domains, e.g., SMT(LIA) formulas. A prototype tool
for SMT(LIA) formulas is also implemented.
The rest of this paper is organized as follows. Preliminary material is in Section 2,
related works in Section 3, the algorithm in Section 4, extensions for SMT(LIA) for-
mulas in Section 5, analysis in Section 6, experimental results in Section 7, and finally,
concluding remarks in Section 8.
2 Preliminaries
Let F (x) denote a propositional logic formula on n variables x = (x1 , . . . , xn ). Let S
and SF denote the whole space (the space of assignments) and the solution space of F ,
respectively. Let #F denote the cardinality of SF , i.e. the number of solutions of F .
(, δ)-bound To count #F , an (, δ) approximation algorithm, > 0 and δ > 0, is
an algorithm which on every input formula F , outputs a number Ỹ such that Pr[(1 +
A New Probabilistic Algorithm for Approximate Model Counting 3
)−1 #F ≤ Ỹ ≤ (1 + )#F ] ≥ 1 − δ. Such an algorithm is called a (, δ)-counter and
the bound is called a (, δ)-bound [23].
Hash Function Let HF be a family of XOR-based bit-level hash functions on Lnthe vari-
ables of a formula F . Each hash function H ∈ HF is of the form H(x) = a0 i=1 ai xi ,
where a0 , . . . , an are Boolean constants. In the hashing procedure Hashing(F), a
function H ∈ HF is generated by independently and randomly choosing ai s from a uni-
form distribution. Thus for an assignment α, it holds that PrH∈HF (H(α) = true) = 21 .
Given a formula F , let Fi denote a hashed formula F ∧H1 ∧· · ·∧Hi , where H1 , . . . , Hi
are independently generated by the hashing procedure.
Satisfiability Query Let Solving(F) denote the satisfiability query of a formula F .
With a target formula F as input, the satisfiability of F is returned by Solving(F).
Enumeration Query Let Counting(F, p) denote the bounded solution enumera-
tion query. With a constraint formula F and a threshold p (p ≥ 2) as inputs, a number s
is returned such that s = min(p − 1, #F ). Specifically, 0 is returned for unsatisfiable
F , or p = 1 which is meaningless.
SMT(BV) Formula SMT(BV) formulas are quantifier-free and fixed-size that combine
propositional logic formulas with constraints of bit-vector theory. For example, ¬(x +
y = 0) ∨ (x = y << 1), where x and y are bit-vector variables, << is the shift-left
operator. It can be regarded as a propositional logic formula ¬A ∨ B that combines bit-
vector constraints A ≡ (x + y = 0) and B ≡ (x = y << 1). To apply hash functions
to an SMT(BV) formula, a bit-vector is bit-blasted to a set of Boolean variables.
SMT(LIA) Formula Similar to SMT(BV) formulas, SMT(LIA) formulas combine
propositional logic formulas with constraints of linear arithmetic theory (i.e., linear
inequalities). For example, ¬(x + y ≥ 0) ∨ (x < y − 1), where x and y are integer
variables. It can be regarded as a propositional logic formula ¬A ∨ B that combines
linear inequalities A ≡ (x + y ≥ 0) and B ≡ (x < y − 1). To apply hash functions to
an SMT(LIA) formula, we introduce a new encoding technique in Section 5.
3 Related Works
[2] showed that almost uniform sampling from propositional constraints, a closely re-
lated problem to constrained counting, is solvable in probabilistic polynomial time with
an NP oracle. Building on this, [9] proposed the first scalable approximate model count-
ing algorithm ApproxMC for propositional formulas. ApproxMC is based on a family
of 2-universal bit-level hash functions that compute XOR of randomly chosen propo-
sitional variables. In the current work, this family of hash functions is adopted, which
was shown to be 3-independent in [21], and is revealed to potentially possess better
properties than expected by the experimental results and the theoretical analysis in the
current work.
The sketch framework of ApproxMC [9, 12] is listed as Algorithm 1. Its inputs are
a formula F and two accuracy parameters T and pivot, where T determines the number
of times ApproxMCCore is invoked, and pivot determines the threshold of the enu-
meration query. The function ApproxMCCore starts from the formula F0 , iteratively
calls Counting and Hashing over each Fi , to cut the space (cell) of all models of
F0 using random hash functions, until the count of Fi is no larger than pivot, then
4 Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, and Xutong Ma
Algorithm 1
1: function A PPROX MC(F , T , pivot)
2: for 1 to T do
3: c ← ApproxMCCore(F , pivot)
4: if (c 6= 0) then AddToList(C, c)
5: end for
6: return FindMedian(C)
7: end function
8: function A PPROX MCC ORE (F , pivot)
9: F0 ← F
10: for i ← 0 to ∞ do
11: s ← Counting(Fi , pivot + 1)
12: if (0 ≤ s ≤ pivot) then return 2i s
13: Hi+1 ← Hashing(F )
14: Fi+1 ← Fi ∧ Hi+1
15: end for
16: end function
breaks out of the loop and adds the approximation 2i s into list C. The main procedure
ApproxMC repeatedly invokes ApproxMCCore and collects the returned values, at
last returning the median number of list C. The general algorithm in [7] is similar to
Algorithm 1, but cuts the cell with dynamically determined proportion instead of the
constant 12 , due to the word-level hash functions. [10] improves ApproxMCCore via
binary search to reduce the number of enumeration queries from linear to logarithmic.
This binary search improvement is orthogonal to our approach.
A recent work [1] considered a special family of shorter XOR-constraints to im-
prove the efficiency of SAT solving while preserving rigourous guarantee. This im-
provement of hash functions is also orthogonal to our approach as we use hash functions
and SAT solving as black boxes. However, it is unknown whether there exist similar
theoretical results like [1].
4 Algorithm
In this section, a new hashing-based algorithm for approximate model counting, with
only satisfiability queries, will be proposed, building on an assumption of a probabilistic
approximate correlation between the model count and the probability of the hashed
formula being unsatisfiable.
Let Fd = F ∧ H1 ∧ · · · ∧ Hd be a hashed formula resulted by iteratively hashing
d times independently over a formula F . Fd is unsatisfiable if and only if no solution
of F satisfies Fd , thus PrFd (Fd is unsat) = PrFd (Fd (α) = f alse, α ∈ SF ). Assume
we have
Pr(Fd is unsat) ≈ (1 − 2−d )#F . (1)
Fd
Then based on Equation (1), an approximation of #F is achieved by taking logarith-
m on the value of PrFd (Fd is unsat), which is estimated in turn by sampling Fd .
A New Probabilistic Algorithm for Approximate Model Counting 5
This is the general idea of our approach. The pseudo-code is presented in Algorithm 2.
The inputs are the target formula F and a constant T which determines the number
of times GetDepth invoked. GetDepth calls Solving and Hashing repeatedly
until an unsatisfiable formula Fdepth is encountered, and returns the depth. Every time
GetDepth returns a depth, the value of C[i] is increased, for all i < depth. At line
9, the algorithm picks a number d such that C[d] is close to T /2, since the error esti-
mation fails when C[d]/T is close to 0 or 1. The final result is returned by the formula
log1−(1/2)d counter
T at line 11.
Algorithm 2 Satisfiability Testing based Approximate Counter (STAC)
1: function STAC(F , T )
2: initialize C[i]s with zeros
3: for t ← 1 to T do
4: depth ← GetDepth(F )
5: for i ← 0 to depth − 1 do
6: C[i] ← C[i] + 1
7: end for
8: end for
9: pick a number d such that C[d] is closest to T /2
10: counter ← T − C[d]
11: return log1−2−d counter T
/* return 0 when d = 0 */
12: end function
13: function G ET D EPTH (F )
14: F0 ← F
15: for i ← 0 to ∞ do
16: b ← Solving(Fi )
17: if (b is false) then return i
18: Hi+1 ← Hashing(Fi )
19: Fi+1 ← Fi ∧ Hi+1
20: end for
21: end function
Note that our approach is based on Equation (1) which is only an assumption. In
Section 6, we provide theoretical analysis, including the bound of the approximation
and the correctness of algorithm, based on the hypothesis. Then in Section 7, experi-
mental results on an extensive set of benchmarks show that the approximation given by
our approach fits the bound well. It indicates that Equation (1) is probably true as it is a
reasonable explanation to the positive results.
Dynamic Stopping Criterion The essence of Algorithm 2 is a randomized sampler over
a binomial distribution. The number of samples is determined by the value of T , which
is pre-computed for a given (, δ)-bound, and we loosen the value of T to meet the
guarantee in theoretical analysis. However, it usually does not loop T times in practice.
A variation with dynamic stopping criterion is presented in Algorithm 3.
Line 2 to 7 is the same as Algorithm 2, still setting T as a stopping rule and ter-
minating whenever t = T . Line 8 to 16 is the key part of this variation, calculating
6 Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, and Xutong Ma
Algorithm 3 STAC with Dynamic Stopping Criterion
1: function STAC DSC(F , T , , δ)
2: initialize C[i]s with zeros
3: for t ← 1 to T do
4: depth ← GetDepth(F )
5: for i ← 0 to depth − 1 do
6: C[i] ← C[i] + 1
7: end for
8: for each d that C[d] > 0 do
9: q ← t−C[d]
t
10: M ← log1−2−d q
q
11: U ← log1−2−d (q − z1−δ q(1−q) )
q t
q(1−q)
12: L ← log1−2−d (q + z1−δ t
)
−1
13: if U < (1 + )M and L > (1 + ) M then
14: return M
15: end if
16: end for
17: end for
18: end function
[L, U ] of an intermediate result M for each
the binomial proportion confidence interval q
cycle. A commonly used formula q ± z1−δ q(1−q) t [4, 34] is adopted, which is justi-
fied by the central limit theorem to compute the 1 − δ confidence interval. However, it
becomes invalid for small sample size or proportion close to 0 or 1. In practice, we also
considered some improvements, e.g., Wilson score interval [35]. The exact count #F
lies in the interval [L, U ] with probability 1 − δ. Combining the inequalities presented
in line 13, the interval [(1 + )−1 M, (1 + )M ] is the (, δ)-bound (if the assumption
of Formula 1 holds). So the algorithm terminates when the condition in line 13 comes
true. The time complexity of Algorithm 3 is still the same as the original algorithm,
though it usually terminates earlier.
Satisfiability And Enumeration Query The bounded counting can be done by negat-
ing solution and calling SAT oracle repeatedly, which is employed by ApproxMC. In
practice, enumerating solutions in this way is not very efficient. In evaluation section,
experimental results show that the average number of SAT calls of ApproxMC is usual-
ly 20 to 30 times to STAC. It may also cause problems while extending to other kinds of
formulas. For example, for linear integer arithmetic formula, inserting solution negation
clauses will exponentially increase the number of calls of LIP solver.
Leap-frogging Strategy Recall that GetDepth is invoked T times with the same argu-
ments, and the loop of line 15 to 20 in the pseudo-code of GetDepth in Algorithm 2
is time consuming for large i. A heuristic called leap-frogging to overcome this bottle-
neck was proposed in [8, 9]. Their experiments indicate that this strategy is extremely
efficient in practice. The average depth d¯ of each invocation of GetDepth is recorded.
A New Probabilistic Algorithm for Approximate Model Counting 7
In all subsequent invocations, the loop starts by initializing i to d¯ − k · offset, where
k ≥ 1. Note that if Fi is unsatisfiable, the algorithm repeatedly decreases i by increas-
ing k and check the satisfiability of the new Fi , until a proper initialization i is found for
satisfiable Fi . In practice, the constant offset is usually set to 5. Theorem 3 in Section 6
shows that the depth computed by GetDepth lies in an interval [d, d + 7] with prob-
ability over 90%. So it suffices to invoke Solving in constant time since the second
iteration.
5 Extensions to SMT(LIA) Formulas
Recall that we employ a family of XOR-based bit-level hash functions on the Lvariables
n
of a formula F . Each such hash function H ∈ HF is of the form H(b) = a0 i=1 ai bi ,
where a0 , . . . , an are Boolean constants. In the hashing procedure, a function H ∈ HF
is generated by independently and randomly choosing ai s from a uniform distribution.
Thus for an assignment α, it holds that PrH∈HF H(α) = true = 12 . To extend the
hash functions to numeric domains, we still have to maintain such probability property
in order to fit our approach.
If we represent a Boolean L variable via integers, i.e., 0 is false, 1 isP
true, intuitive-
n n
ly, the XOR hash function a0 i=1 ai bi can be represented by (α0 + i=1 αi × xi )
mod 2, where α0 , . . . , αn are {0, 1}-constants and x1 , . . . , xn are {0, 1}-variables.
Then we extend the domain from {0, 1} to integers directly. Consider a formula F
over integer domain. Let IF denote the family of hash functions for the integer domain
and each I ∈ IF is of the form
n
X
I(x) = (α0 + αi × xi ) mod 2.
i=1
It is easy to see that PrI∈IF I(α) = true = 21 is hold for any assignment α of F as
well.
To extend our approach to the integer domain, it is necessary to adapt the new
integer hash function to satisfiability query. However, in practice, the modulo operation
is not supported in many satisfiability checkers, e.g., SMT(LIA) solvers. We introduce
a new technique to encode the modulo operation via arithmetic operations. Given a
simple constraint that contains a modulo operation,
f (x) mod m = n, (2)
where f (x) is a formula over variables x, m and n are constants. We introduce a new
integer variable y. Then consider the following constraint
f (x) = m × y + n. (3)
Obviously, Equation 2 is satisfiable if and only if Equation 3 is satisfiable. If f (x) is a
linear arithmetic formula, Equation 3 is able to be solved by linear arithmetic
Pn solvers.
In conclusion, we transform the hash function constraint (α0 + i=1 αi × xi )
mod 2 = 1 into a linear arithmetic constraint
Xn
(α0 + αi × xi ) = 2 × y + 1.
i=1
8 Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, and Xutong Ma
It enables the extension of our approach to SMT(LIA) formulas. A prototype tool for
SMT(LIA) formulas is also implemented.
6 Analysis
In this section, we assume Equation (1) holds. Based on this assumption, theoretical
results on the error estimation of our approach are presented. For lack of space, we
omit proofs in this section.
Recall that in Algorithm 2, #F is approximated by a value log1−2−d counter
T . Let qd
denote the value of (1 − 2−d )#F . We obtain that Pr(Fd is unsat) = qd for a randomly
generated formula Fd . This is justified by Equations (1). Since the ratio counter
T in
Algorithm 2 is a proportion of successes in a Bernoulli trial process, which is used
to estimate the value of qd . Then counter is a random variable following a binomial
distribution B(T, qd ).
Theorem 1. Let z1−δ be the 1 − δ quantile of N(0, 1) and
!
z1−δ 2 z1−δ 2
T = max d( ) e, d( (1+)−1 ) )e . (4)
2qd (1 − qd ) 2(q − qd )
d
#F
Then Pr[ 1+ ≤ log1−2−d counter
T ≤ (1 + )#F ] ≥ 1 − δ.
Proof. By above discussions, the ratio counter
T is the proportion of successes in a Ber-
noulli trial process which follows the distribution B(T, qd ). Then we use
q the approxi-
mate formula of a binomial proportion confidence interval qd ± z1−δ qd (1−q T
d)
, i.e.,
q q
Pr[qd − z1−δ qd (1−q
T
d)
≤ counter
T ≤ qd + z1−δ qd (1−q T
d)
] ≥ 1 − δ. The log function
is monotone, so we only have to consider the following two inequalities:
r
qd (1 − qd )
log1−2−d (qd − z1−δ ) ≤ (1 + )#F, (5)
T
r
qd (1 − qd )
(1 + )−1 #F ≤ log1−2−d (qd + z1−δ ). (6)
T
We first consider Equation (5). By substituting log1−2−d qd for #F , we have
r
qd (1 − qd )
log1−2−d (qd − z1−δ ) ≤ (1 + ) log1−2−d qd
T
r
qd (1 − qd ) (1+)
⇔ qd − z1−δ ≥ qd
T
r
qd (1 − qd )
⇔ qd (1 − qd ) ≥ z1−δ
T
z1−δ 2
⇔T ≥( ) qd (1 − qd ).
qd (1 − qd )
A New Probabilistic Algorithm for Approximate Model Counting 9
qd (1 − qd ) ≤ 21 . Therefore, T = d( 2qdz(1−q
p 2
Since 0 ≤ qd ≤ 1, we have 1−δ
) ) e ≥
d
( qd z(1−q
1−δ 2
) qd (1 − qd ).
d)
We next consider Equation (6). Similarly, we have
r
qd (1 − qd )
log1−2−d (qd + z1−δ ) ≥ (1 + )−1 log1−2−d qd
T
r
qd (1 − qd ) 1/(1+)
⇔ qd + z1−δ ≤ qd
T
z1−δ
⇔ T ≥ ( 1/(1+) )2 qd (1 − qd ).
qd − qd
So Equation (4) implies Equations (5) and (6).
Theorem 1 shows that the result of Algorithm 2 lies in the interval [(1+)−1 #F, (1+
)#F ] with probability at least 1 − δ when T is set to a proper value. So we focus on
the possible smallest value of T in subsequent analysis.
The next two lemmas are easy to show by derivations.
z1−δ − 1
Lemma 1. 2x(1−x ) is monotone increasing and monotone decreasing in [(1+) , 1]
1
and [0, (1 + )− ] respectively.
z1−δ
Lemma 2. 2(x1/(1+) −x)
is monotone increasing and monotone decreasing in [(1 +
1+ 1+
)− , 1] and [0, (1 + )− ] respectively.
Theorem 2. If #F > 5, then there exists a proper integer value of d such that qd ∈
[0.4, 0.65].
Proof. Let x denote the value of qd = (1 − 21d )#F , then we have (1 − 2d+1
1
)#F =
1
#F
( 12 + x 2 )#F . Consider the derivation
1 1 1
1
1 x #F 1 x #F x #F d
d 1 x #F #F
d#F ( 2 + 2 ) =( + )#F ln ( + ) ln x (#F −1 ).
2 2 2 2 2 d#F
1 1 1
#F #F #F
Note that ( 21 + x 2 )#F and x 2 are the positive terms and ln ( 12 + x 2 ), ln x and
d −1
d#F (#F ) are the negative terms. Therefore, the derivation is negative, i.e., ( 12 +
1 1
x #F #F
2 ) is monotone decreasing with respect to #F . In addition, ( 12 + x25 )5 is the
upper bound when #F ≥ 5.
1
1
Let x = 0.4, then (1 − 2d+1 )#F ≤ ( 21 + 0.42 5 )5 ≈ 0.65. Since (1 − 210 )#F = 0 and
1 #F
limd→+∞ (1 − 2d ) = 1 and (1 − 21d )#F is continuous with respect to d, we consider
the circumstances close to the interval [0.4, 0.65]. Assume there exists an integer σ such
that (1 − 21σ )#F < 0.4 and (1 − 2σ+1
1
)#F > 0.65. According to the intermediate value
1
theorem, we can find a value e > 0 such that (1 − 2σ+e )#F = 0.4. Obviously, we have
1 #F
(1 − 2σ+e+1 ) ≤ 0.65 which is contrary with the monotone decreasing property.
10 Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, and Xutong Ma
From Theorem 2 and Lemma 1 and 2, it suffices to consider the results of Equa-
tion (4) when qd = 0.4 and qd = 0.65. For example, T = 22 for = 0.8 and δ = 0.2,
T = 998 for = 0.1 and δ = 0.1, etc. We therefore pre-computed a table of the value
of T . The proof of next theorem is omitted.
Theorem 3. There exists an integer d such that qd < 0.05 and qd+7 > 0.95.
Let depth denote the result of GetDepth in Algorithm 2. Then Fd is unsatisfiable
only if d ≥ depth. Theorem 3 shows that there exists an integer d such that Pr(depth <
d) < 0.05 and Pr(depth < d + 7) > 0.95, i.e., Pr(d ≤ depth ≤ d + 7) > 0.9. So in
most cases, the value of depth lies in an interval [d, d + 7]. Also, it is easy to see that
log2 #F lies in this interval as well. The following theorem is obvious now.
Theorem 4. Algorithm 2 runs in time linear in log2 #F relative to an NP-oracle.
7 Evaluation
To evaluate the performance and effectiveness of our approach, two prototype imple-
mentations STAC CNF and STAC BV with dynamic stopping criterion for proposition-
al logic formulas and SMT(BV) formulas are built respectively. We considered a wide
range of benchmarks from different domains: grid networks, plan recognition, DQM-
R networks, Langford sequences, circuit synthesis, random 3-CNF, logistics problems
and program synthesis [29, 24, 9, 7] 6 . For lack of space, we only list a part of results
here. All our experiments were conducted on a single core of an Intel Xeon 2.40GHz
(16 cores) machine with 32GB memory and CentOS6.5 operating system.
7.1 Quality of Approximation
Recall that our approach is based on Equation (1) which has not been proved. So we
would like to see whether the approximation fits the bound. We experimented 100 times
on each instance.
In Table 1, column 1 gives the instance name, column 2 the number of Boolean vari-
ables n, column 3 the exact counts #F , and column 4 the interval [1.8−1 #F, 1.8#F ].
The frequencies of approximations that lie in the interval [1.8−1 #F, 1.8#F ] in 100
times of experiments are presented in column 5. The average time consumptions, aver-
age number of iterations, and average number of SAT query invocations are presented
in column 6, 7 and 8 respectively, which also indicate the advantages of our approach.
Under the dynamic stopping criterion, the counts returned by our approach should
lie in an interval [1.8−1 #F, 1.8#F ] with probability 80% for = 0.8 and δ = 0.2.
The statistical results in Table 1 show that the frequencies are around 80 for 100-times
experiments which fit the 80% probability. The average number of iterations T̄ listed
in Table 1 is smaller than the loop termination criterion T = 22 which is obtained via
Formula 4, indicating that the dynamic stopping technique significantly improves the
6
Our tools STAC CNF and STAC BV and the suite of benchmarks are available at
https://github.com/bearben/STAC
A New Probabilistic Algorithm for Approximate Model Counting 11
Table 1. Statistical results of 100-times experiments on STAC CNF ( = 0.8, δ = 0.2)
Instance n #F [1.8−1 #F, 1.8#F ] Freq. t̄ (s) T̄ Q̄
6 5 6
special-1 20 1.0 × 10 [5.8 × 10 , 1.9 × 10 ] 82 0.3 12.2 86.7
special-2 20 1 [0.6, 1.8] 86 0.6 12.6 37.6
special-3 25 3.4 × 107 [1.9 × 107 , 6.0 × 107 ] 82 11.2 11.8 90.1
5step 177 8.1 × 104 [4.5 × 104 , 1.5 × 105 ] 90 0.1 11.9 80.5
blockmap 05 01 1411 6.4 × 102 [3.6 × 102 , 1.2 × 103 ] 84 1.1 12.0 73.8
blockmap 05 02 1738 9.4 × 106 [5.2 × 106 , 1.7 × 107 ] 89 12.7 11.8 87.7
blockmap 10 01 11328 2.9 × 106 [1.6 × 106 , 5.2 × 106 ] 83 80.3 12.0 85.0
fs-01 32 7.7 × 102 [4.3 × 102 , 1.4 × 103 ] 80 0.02 12.6 76.2
or-50-10-10-UC-20 100 3.7 × 106 [2.0 × 106 , 6.6 × 106 ] 77 7.7 12.0 86.1
or-60-10-10-UC-40 120 3.4 × 106 [1.9 × 106 , 6.1 × 106 ] 91 3.5 12.1 86.0
efficiency. In addition, the values of T̄ appear to be stable for different instances, hinting
that there exists a constant upper bound on T which is irrelevant to instances.
Intuitively, our approach may start to fail on “loose” formulas, i.e., with an “in-
finitesimal” fraction of non-models. Instance special-1 and special-3 are such “loose”
formulas where special-1 has 220 models with only 20 variables and special-3 has
225 − 1 models with 25 variables. Instance special-2 is another extreme case which
only has one model. The results in Table 1 demonstrate that STAC CNF also works fine
on these extreme cases.
Table 2. Statistical results of 100-times experiments on STAC CNF ( = 0.2, δ = 0.1)
Instance n #F [1.2−1 #F, 1.2#F ] Freq. t̄ (s) T̄ Q̄
6 5 6
special-1 20 1.0 × 10 [8.7 × 10 , 1.3 × 10 ] 86 4.0 179 1023
special-2 20 1 [0.8, 1.2] 91 0.1 179 540
special-3 25 3.4 × 107 [2.8 × 107 , 4.0 × 107 ] 91 138 178 1029
5step 177 8.1 × 104 [6.8 × 104 , 9.8 × 105 ] 96 1.9 190 1078
blockmap 05 01 1411 6.4 × 102 [5.3 × 102 , 7.7 × 102 ] 94 17.1 190 1069
blockmap 05 02 1738 9.4 × 106 [7.9 × 106 , 1.1 × 107 ] 87 281 193 1088
blockmap 10 01 11328 2.9 × 106 [2.4 × 106 , 3.5 × 106 ] 93 1371 180 1034
fs-01 32 7.7 × 102 [6.4 × 102 , 9.2 × 102 ] 91 0.1 172 975
or-50-10-10-UC-20 100 3.7 × 106 [3.1 × 106 , 4.4 × 106 ] 90 140 166 925
or-60-10-10-UC-40 120 3.4 × 106 [2.8 × 106 , 4.1 × 106 ] 92 66 167 949
We considered another pair of parameters = 0.2, δ = 0.1. Then the interval
should be [1.2−1 #F, 1.2#F ] and the probability should be 90%. Table 2 shows the
results on such parameter setting. The frequencies that the approximation lies in interval
[1.2−1 #F, 1.2#F ] are all around or over 90 which fits the 90% probability.
We also conducted 100-times experiments on SMT(BV) problems and the results
show that STAC BV is also promising. Table 3 similarly shows the results of 100-times
experiments on STAC BV. Its column 2 gives the sum of widths of all bit-vector vari-
12 Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, and Xutong Ma
ables (Boolean variable is counted as a bit-vector of width 1) instead. The statistical
results demonstrate that the dynamic stopping criterion is also promising on SMT(BV)
problems.
Table 3. Statistical results of 100-times experiments on STAC BV ( = 0.8, δ = 0.2)
Instance TB. #F [1.8−1 #F, 1.8#F ] Freq. t̄ (s) T̄ Q̄
6 6 6
FINDpath1 32 4.1 × 10 [2.3 × 10 , 7.3 × 10 ] 83 27.5 12.4 88.0
queue 16 8.4 × 10 [4.7 × 10, 1.5 × 102 ] 75 1.7 12.0 70.6
getopPath2 24 8.1 × 103 [4.5 × 103 , 1.5 × 104 ] 88 2.7 12.2 79.5
coloring 4 32 1.8 × 109 [1.0 × 109 , 3.3 × 109 ] 76 51.9 12.0 96.1
FISCHER2-7-fair 240 3.0 × 104 [1.7 × 104 , 5.4 × 104 ] 79 149 11.8 79.8
case2 24 4.2 × 106 [2.3 × 106 , 7.6 × 106 ] 79 16.5 12.4 89.3
case4 16 3.3 × 104 [1.8 × 104 , 5.9 × 104 ] 87 2.2 12.5 85.2
case7 18 1.3 × 105 [7.3 × 104 , 2.4 × 105 ] 83 2.9 12.4 84.1
case8 24 8.4 × 106 [4.7 × 106 , 1.5 × 107 ] 82 14.4 12.1 91.1
case11 15 1.6 × 104 [9.1 × 103 , 2.9 × 104 ] 76 2.1 12.0 81.2
7.2 Performance Comparison with (, δ)-counters
We compared our tools with ApproxMC2 [10] and SMTApproxMC [7] which are
hashing-based (, δ)-counters. Both STAC CNF and ApproxMC2 use CryptoMini-
SAT [31], an efficient SAT solver designed for XOR clauses. STAC BV and SMT-
ApproxMC use the state-of-the-art SMT(BV) solver Boolector [5].
30000 30000
3000 3000
300 300
SMTApproxMC
ApproxMC2
30 30
3 3
0.3 0.3
0.03 0.03
0.03 0.3 3 30 300 3000 30000 0.03 0.3 3 30 300 3000 30000
STAC_CNF STAC_BV
Fig. 1. Performance comparison between Fig. 2. Performance comparison between
STAC CNF and ApproxMC2 STAC BV and SMTApproxMC
A New Probabilistic Algorithm for Approximate Model Counting 13
We first conducted experiments with = 0.8, δ = 0.2 and 8 hours timeout which
are also used in evaluation in previous works [10, 7]. Figure 1 presents a comparison
on performance between STAC CNF and ApproxMC2. Each point represents an in-
stance, whose x-coordinate and y-coordinate are the running times of STAC CNF and
ApproxMC2 on this instance, respectively. The figure is in logarithmic coordinates and
demonstrates that STAC CNF outperforms ApprxMC2 by about one order of magni-
tude. Figure 2 presents a similar comparison on performance between STAC BV and
SMTApproxMC, showing that STAC BV outperforms SMTApproxMC by one or two
orders of magnitude. Furthermore, the advantage enlarges as the scale grows.
Table 4. Performance comparison between STAC CNF and ApproxMC2 with different pairs of
(, δ) parameters
XX
XXX Instance blockmap
fs-01 5step ran5 ran6 ran7
(, δ) XXX
X 05 01 05 02 10 01
Time Ratio 1.11 3.99 1.22 3.00 3.83 6.53 8.24 5.57
(0.8, 0.3)
#Calls Ratio 22.60 39.02 17.91 19.12 23.11 22.53 21.28 23.68
Time Ratio 1.84 6.16 2.44 2.80 6.05 9.61 15.41 7.37
(0.8, 0.2)
#Calls Ratio 26.70 34.68 25.16 33.46 27.24 33.35 38.22 30.94
Time Ratio 2.27 7.36 3.72 5.25 12.62 9.60 9.54 8.19
(0.8, 0.1)
#Calls Ratio 44.88 48.26 40.01 49.40 43.03 46.12 44.84 52.63
Time Ratio 0.75 1.37 0.42 3.00 5.04 1.97 2.31 2.74
(0.4, 0.3)
#Calls Ratio 17.75 36.20 14.69 16.40 27.63 21.07 27.34 21.63
Time Ratio 0.77 1.44 0.86 4.50 7.70 2.82 1.77 3.02
(0.4, 0.2)
#Calls Ratio 20.91 26.35 29.16 26.72 40.66 26.49 27.82 28.94
Time Ratio 1.08 2.57 1.29 4.90 7.09 3.84 3.43 3.11
(0.4, 0.1)
#Calls Ratio 37.16 46.28 39.40 31.99 39.36 41.02 35.88 34.11
Time Ratio 0.42 0.47 0.23 5.08 3.79 1.26 1.14 1.81
(0.2, 0.3)
#Calls Ratio 13.75 20.82 24.35 13.37 19.74 25.20 19.19 20.06
Time Ratio 0.57 0.92 0.26 8.42 3.37 2.07 1.50 2.45
(0.2, 0.2)
#Calls Ratio 21.80 29.62 25.60 21.83 21.59 25.88 22.72 22.98
Time Ratio 0.87 0.92 0.44 16.69 3.17 3.61 2.27 2.60
(0.2, 0.1)
#Calls Ratio 27.86 29.91 33.36 34.17 31.58 40.81 29.01 29.90
Table 4 presents more experimental results with (, δ) parameters other than ( =
0.8, δ = 0.2). Nine pairs of parameters were experimented. “Time Ratio” represents the
ratio of the running times of ApproxMC2 to STAC CNF. “#Calls Ratio” represents the
ratio of the number of SAT calls of ApproxMC2 to STAC CNF. The results show that
ApproxMC2 gains advantage as decreases and STAC CNF gains advantage as δ de-
creases. On the whole, ApproxMC2 gains advantage when and δ both decrease. Note
that the numbers of SAT calls represent the complexity of both algorithms. In Table 4,
#Calls Ratio is more stable than Time Ratio among different pairs of parameters and
also different instances. It indicates that the difficulty of NP-oracle is also an important
factor of running time performance.
14 Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, and Xutong Ma
8 Conclusion
In this paper, we propose a new hashing-based approximate algorithm with dynamic
stopping criterion. Our approach has two key strengths: it requires only one satisfia-
bility query for each cut, and it terminates once meeting the criterion of accuracy. We
implemented prototype tools for propositional logic formulas and SMT(BV) formu-
las. Extensive experiments demonstrate that our approach is efficient and promising.
Despite that we are unable to prove the correctness of Equation (1), the experimental
results fit it quite well. This phenomenon might be caused by some hidden properties
of the hash functions. To fully understand these functions and their correlation with the
model count of the hashed formula might be an interesting problem to the community.
In addition, extending the idea in this paper to count solutions of other formulas is also
a direction of future research.
References
1. D. Achlioptas and P. Theodoropoulos. Probabilistic model counting with short xors. In Proc.
of SAT, pages 3–19, 2017.
2. M. Bellare, O. Goldreich, and E. Petrank. Uniform generation of NP-witnesses using an
NP-oracle. Inf. Comput., 163(2):510–526, 2000.
3. V. Belle, G. V. Broeck, and A. Passerini. Hashing-based approximate probabilistic inference
in hybrid domains. In Proc. of UAI, pages 141–150, 2015.
4. L. D. Brown, T. T. Cai, and A. Dasgupta. Interval estimation for a binomial proportion.
Statistical Science, 16(2):101–133, 2001.
5. R. Brummayer and A. Biere. Boolector: An efficient SMT solver for bit-vectors and arrays.
In Proc. of TACAS, pages 174–177, 2009.
6. S. Chakraborty, D. J. Fremont, K. S. Meel, S. A. Seshia, and M. Y. Vardi. Distribution-aware
sampling and weighted model counting for SAT. In Proc of AAAI, pages 1722–1730, 2014.
7. S. Chakraborty, K. S. Meel, R. Mistry, and M. Y. Vardi. Approximate probabilistic inference
via word-level counting. In Proc. of AAAI, pages 3218–3224, 2016.
8. S. Chakraborty, K. S. Meel, and M. Y. Vardi. A scalable and nearly uniform generator of
SAT witnesses. In Proc. of CAV, pages 608–623, 2013.
9. S. Chakraborty, K. S. Meel, and M. Y. Vardi. A scalable approximate model counter. In
Proc. of CP, pages 200–216, 2013.
10. S. Chakraborty, K. S. Meel, and M. Y. Vardi. Algorithmic improvements in approximate
counting for probabilistic inference: From linear to logarithmic SAT calls. In Proc. of IJCAI,
pages 3569–3576, 2016.
11. M. Chavira and A. Darwiche. On probabilistic inference by weighted model counting. Artif.
Intell., 172(6-7):772–799, 2008.
12. D. Chistikov, R. Dimitrova, and R. Majumdar. Approximate counting in SMT and value
estimation for probabilistic programs. In Proc. of TACAS, pages 320–334, 2015.
13. C. Domshlak and J. Hoffmann. Probabilistic planning via heuristic forward search and
weighted model counting. J. Artif. Intell. Res. (JAIR), 30:565–620, 2007.
14. S. Ermon, C. P. Gomes, A. Sabharwal, and B. Selman. Embed and project: Discrete sampling
with universal hashing. In Advances in Neural Information Processing Systems 26, pages
2085–2093, 2013.
15. A. Filieri, C. S. Pasareanu, and W. Visser. Reliability analysis in symbolic pathfinder: A brief
summary. In Proc. of ICSE, pages 39–40, 2014.
A New Probabilistic Algorithm for Approximate Model Counting 15
16. A. Filieri, C. S. Pasareanu, and G. Yang. Quantification of software changes through proba-
bilistic symbolic execution (N). In Proc. of ASE, pages 703–708, 2015.
17. M. Fredrikson and S. Jha. Satisfiability modulo counting: a new approach for analyzing
privacy properties. In Proc. of CSL-LICS, pages 42:1–42:10, 2014.
18. J. Geldenhuys, M. B. Dwyer, and W. Visser. Probabilistic symbolic execution. In Proc. of
ISSTA, pages 166–176, 2012.
19. K. Gleissenthall, B. Köpf, and A. Rybalchenko. Symbolic polytopes for quantitative inter-
polation and verification. In Proc. of CAV, pages 178–194, 2015.
20. C. P. Gomes, A. Sabharwal, and B. Selman. Model counting: A new strategy for obtaining
good bounds. In Proc. of AAAI, pages 54–61, 2006.
21. C. P. Gomes, A. Sabharwal, and B. Selman. Near-uniform sampling of combinatorial spaces
using XOR constraints. In Advances in Neural Information Processing Systems 19, pages
481–488, 2006.
22. A. Ivrii, S. Malik, K. S. Meel, and M. Y. Vardi. On computing minimal independent support
and its applications to sampling and counting. Constraints, 21(1):41–58, 2016.
23. R. M. Karp, M. Luby, and N. Madras. Monte-carlo approximation algorithms for enumera-
tion problems. J. Algorithms, 10(3):429–448, 1989.
24. L. Kroc, A. Sabharwal, and B. Selman. Leveraging belief propagation, backtrack search, and
statistics for model counting. Annals of OR, 184(1):209–231, 2011.
25. S. Liu and J. Zhang. Program analysis: from qualitative analysis to quantitative analysis. In
Proc. of ICSE, pages 956–959, 2011.
26. K. S. Meel, M. Y. Vardi, S. Chakraborty, D. J. Fremont, S. A. Seshia, D. Fried, A. Ivrii, and
S. Malik. Constrained sampling and counting: Universal hashing meets SAT solving. In
Proceedings of Workshop on Beyond NP(BNP), 2016.
27. Q. Phan, P. Malacaria, C. S. Pasareanu, and M. d’Amorim. Quantifying information leaks
using reliability analysis. In Proc. of SPIN, pages 105–108, 2014.
28. D. Roth. On the hardness of approximate reasoning. Artif. Intell., 82(1-2):273–302, 1996.
29. T. Sang, P. Beame, and H. A. Kautz. Performing bayesian inference by weighted model
counting. In Proc. of AAAI, pages 475–482, 2005.
30. M. Sipser. A complexity theoretic approach to randomness. In Proc. of the 15th Annual
ACM Symposium on Theory of Computing, pages 330–335, 1983.
31. M. Soos, K. Nohl, and C. Castelluccia. Extending SAT solvers to cryptographic problems.
In Proc. of SAT, pages 244–257, 2009.
32. L. J. Stockmeyer. The complexity of approximate counting (preliminary version). In Proc.
of the 15th Annual ACM Symposium on Theory of Computing, pages 118–126, 1983.
33. L. G. Valiant. The complexity of enumeration and reliability problems. SIAM J. Comput.,
8(3):410–421, 1979.
34. S. Wallis. Binomial confidence intervals and contingency tests: Mathematical fundamentals
and the evaluation of alternative methods. Journal of Quantitative Linguistics, 20(3):178–
208, 2013.
35. E. B. Wilson. Probable inference, the law of succession and statistical inference. Journal of
the American Statistical Association, 22(158):209–212, 1927.