Structural Bit-vector Model Counting Seonmo Kim and Stephen McCamant University of Minnesota, Minneapolis, Minnesota, U.S.A. {smkim, mccamant}@cs.umn.edu Abstract Various approximate model counting techniques have been proposed and are used in many applications such as probabilistic inference and quantitative information-flow secu- rity. The hashing-based technique is a well-known approach and can be more scalable than exact model counting techniques. However, its performance is highly dependent on the performance of a decision procedure (SAT or SMT solver) and adding numerous hash- ing constraints to a formula might cause a solver to perform poorly. We propose a model counting technique which computes lower and upper bounds of the number of solutions to an SMT formula by analyzing the structure of the formula, which means this approach does not rely on a decision procedure. Our algorithm runs in polynomial time and gives firm lower and upper bounds unlike other approximate model counters that compute probabilistic bounds. We compare our algorithm with state-of-the- art model counters and our experiments show that our approach is faster than others and provides a trade-off between computational effort and the precision of results. 1 Introduction Model counting is a quantitative generalization of the satisfiability problem that asks for the number of satisfying assignments for a formula. Some of the many applications of model count- ing include combinatorics, safety analysis, probabilistic inference, and quantitative information- flow analysis of software. Model counting is also closely connected to uniform random sampling of formula solutions. However, exact model counting even just for quantifier-free Boolean for- mulas (#SAT) is complete for the complexity class #P which is believed to be intractable. Approximations to an exact model count are useful in many applications, so the difficulty of exact model counting motivates exploring approximation algorithms. The best-known approaches in recent research use hashing to reduce approximate model counting to an adaptive sequence of satisfiability queries covering subsets of the solution space. These algorithms provide probabilistic bounds on the accuracy of their approximation, and they can take advantage of advances in satisfiability solving (both SAT and SMT). However these approaches still have limited scalability in practice: they require a large number of satisfiability queries to achieve tight bounds, and hashing can make individual queries much more expensive, given the complex interactions between hashing constraints and solver optimizations. Also valuable but less developed are approximation algorithms which achieve guaranteed efficiency and sound bounds, at the expense of not providing an accuracy guarantee. This trade-off can be achieved using algorithms similar to ones used in static program analysis that derive lower and/or upper bounds following the syntactic structure of a formula rather than using semantic decision procedure queries. We refer to these as “structural” approximate model counting algorithms. Previous structural model counting algorithms have been specialized for narrow domains, or have been built into larger systems in ways that are not easily reusable. In this work, we build a new structural approximate model counting tool for quantifier-free SMT formulas over the theory of bit vectors (SMT-LIB QF BV), one of the most common theories used to model François Bobot, Tjark Weber (eds.); SMT 2020, pp. 26–36 Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). Structural Bit-Vector Model Counting Kim and McCamant bounded arithmetic and software semantics. We also provide a commonly useful generalization known as projected model counting, in which a user can specify a subset of the variables in a formula over which a model should be counted. Our tool uses algorithms which build on the partial description of a previous closed-source tool [16], but we needed to develop new structural rules for cases that were missing or restricted in previous work. We extend the algorithm to cover a more complete set of bit-vector operators, and to use both the signed and unsigned orderings of bit vectors. However our current implementation, like Martin’s [16], is limited to conjunctions and not arbitrary Boolean combinations of bit-vector relations. This matches the needs, for instance, of typical single-path symbolic execution, where a path condition is a conjunction of branch conditions, each of which is an equality or inequality over numeric (e.g. bit-vector) terms. We have built a standalone tool, SMC, that operates on input in the standard SMT-LIB2 format, and which we have open-source. We have checked the correctness of the propagation rules for each type of bit-vector expression via bounded exhaustive testing. We empirically compare SMC’s performance with representative state-of-the-art exact and approximate model counting tools. The results show that SMC’s performance scales much better than these other tools, and that the sound upper and lower model-count bounds that it provides are often usefully accurate. 2 Related Work We categorize previous model-counting tools based on exact approaches, hashing-based approx- imation, and structural approximation. Exact model counting Exact model counting for propositional formulas (#SAT) typically uses techniques related to SAT solving: intuitively, a #SAT algorithm must traverse the entire search space even for a satisfiable formula, instead of stopping at the first satisfying assignment as a SAT solver does. The counting process is optimized by caching information about the number of solutions for sub-formulas that appear repeatedly in the total. Relsat [4], Cachet [19], and sharpSAT [24] are some examples of tools based on varieties of caching. dSharp [18] builds on sharpSAT and also computes a conversion of Boolean formula to a restricted normal form known as d-DNNF (deterministic, decomposable negation normal form) which facilitates other operations. dSharp p [2] further builds on dSharp to support projected model counting; it is the exact model counting tool we compare with in our evaluation below. Two other notable more recent systems are countAntom [5], which uses a parallel algorithm, and Ganak [20], which uses probabilistic hashing to save space, but still produces an exact model count with a guaranteed minimum probability. Hashing-based model counting The core principle that enables hashing-based approxi- mation was first deployed for theoretical results, notably by Sipser [21], Stockmeyer [23], and Valiant and Vazirani [25]. It was first applied to build model counting tools by Gomes et al. [12], who gave an approach that probablistically checked a hypothesized lower or upper bound. Later systems achieved complete automation by designing outer-loop algorithms to search over model count hypotheses. The best known tool of this kind is ApproxMC [7] and its successors includ- ing ApproxMC2 [8], and BIRD/ApproxMC3 [22], and a projecting variant ApproxMC-p [14]. SearchMC [13] reduces the number of queries needed by keeping a statistical estimation of the model count, and also implements a mode that can apply directly wrap an SMT solver (tools 27 Structural Bit-Vector Model Counting Kim and McCamant (declare-fun x () (_ BitVec 8)) (declare-fun y () (_ BitVec 8)) (assert (= y (bvadd (bvand x 15) 4))) Figure 1: Simple Example designed solely for #SAT require eager bit-blasting). We take SearchMC as the representative of hashing-based approximate model counters in our evaluation. Structural model counting Structural approaches to approximate model counting that can provide non-probabilistic bounds (but not guaranteed precision) have seen relatively less tool development. The most direct predecessor of our work in this paper is the FSCB (Fast Solution Count Bounder) algorithm of Martin [16], which as far as we are aware was applied only as part of symbolic execution system to estimate the amount of information revealed by bug reports [6]. Martin’s implementation was not available, but we used the description in his technical report as a starting point for the system we developed, as described in more detail in Section 3. Other previous structural model-counting systems have been specialized for other domains. Luu et al. [15] build a model counter for string constraints such as arise in symbolic execution of high-level languages like JavaScript; their approach is based on generating functions. Aydin et al.’s MT-ABC [1] uses a combination of structural and automaton-based algorithms for constraints that can include a mix of strings and linear arithmetic. Meng and Smith’s two-bit-pattern technique [17] is a hybrid of structural and exact counting approaches to #SAT. It structurally over-approximates the model count by determining, for every pair of bits in a formula, what values they can have in isolation (using many small satisfiability queries). Then the combination of these constraints is a 2CNF formula, which the authors found could be model-counted efficiently in practice (though general 2CNF model counting is still #P-hard). 3 Structural Model Counter The Structural Model Counter (SMC1 ) takes as input an SMT-LIB2 formula which consists of variables and assertions. It outputs lower and upper bounds of satisfying assignments that make a given formula true. First, we describe how this structural model counting technique works with a simple example in Fig 1. Since x and y are 8-bit variables, the model counts of two variables are both 256 when they are declared. Then we parse an assertion to analyze the structure of the formula. (bvand x 15) has the minimum 0 and the maximum 15. This generates 16 distinct values. Adding 4 makes the minimum 4, the maximum 19 and still 16 distinct values. This is equal to y thus y has 16 distinct values. The model count of this formula is 256 since x has 256 distinct values and x determines y. This shows a simple process of the structure model counting. In this section, we describe this algorithm in detail, its correctness, some current limitations and differences from the previous work. 1 The source code and benchmarks are available at: https://github.com/seonmokim/smc 28 Structural Bit-Vector Model Counting Kim and McCamant 3.1 Algorithm The main algorithm is mostly inspired by Martin’s FSCB (Fast Solution Count Bounder) algo- rithm [16]. He proposed this idea to be a fast algorithm that can handle complex expressions such as standard arithmetic or bit shifts. However, FSCB does not consider signed data types and the source code is not available. We extend FSCB to handle both unsigned and signed data types and cover more operators including signed division, signed less-than, signed greater-than and so on. Also, we improve the idea to compute tighter bounds and verify its correctness using small-sized unit tests exhaustively. In this section, we describe two steps of our algorithm. It first computes the bounds for each individual assertion, and then merges them for the model count of a given formula. 3.1.1 Per-Assertion Bounds and Analysis When a variable is declared or an expression is generated, we create a corresponding node to rep- resent this variable or expression. Each node contains elements as [ul, uh, sl, sh, lc, hc, hom, vars]. Since we only consider bit vectors in SMT-LIB2 format, we compute both cases, unsigned and signed representations, in a node. ul, uh, sl and sh are the unsigned mini- mum (low), the unsigned maximum (high), the signed minimum and the signed maximum of the node, respectively. lc and hc are the low cardinality (lower bound), the high cardinality (upper bound) of the node, respectively. We select the bounds which have a shorter interval between the unsigned and signed bounds since both the bounds are sound and tighter bounds give a better precision. hom is a flag such that a node is homogeneous only if every image has the same number of preimages. For example, (bvand x 15) is homogeneous since it generates 16 distinct values and each value (image) has the same number of preimages (16 cases if x is 8-bit). This flag is useful when computing bounds more precisely with a constant value. For example, let us assume that we have (= (bvand x 15) 0) and x is 8-bit. (bvand x 15) should be zero to satisfy this assertion and one value of (bvand x 15) maps to 16 preimages of x. Therefore, this can be computed easily as x has exactly 16 distinct values to satisfy this assertion. vars is a set of variables which presents in an assertion. As we described above, we represent a signed and unsigned values in a single node. One reason that we need both representations is that we want to handle signed operators such as signed division, signed less-than, signed greater-than and so on. Another reason is the ways of computing signed values and unsigned values are different. Therefore, we maintain both representations in every operation and give a warning whenever SMC sees a conflict case. SMC first replaces each constant or variable from an expression with the corresponding node. If it is a constant c, the node can be represented as [c, c, c, c, 1, 1, true, {}]. Note that if c is a binary or hexadecimal number, we convert the number using the two’s complement. The next step is that SMC breaks down an expression tree and generates a node based on the expression rules starting from the sub-expressions. SMC determines how to compute the node values from the expression rules for each supported operation. We can extend SMC to support additional operations by adding new operation rules. We only show a subset of the operation rules here. Pseudocode for bvadd is shown in Fig 2. When the tool reaches a bvadd operation, it first checks whether the variables are both constant values. This checking applies to other operations as well and we can easily compute all the values if they are both constant values. Next we check that the answer might be an arithmetic positive or negative overflow. If this occurs, we set ul and uh as the minimum and the maximum of the variable, respectively, based on its bit-width unless the variables are both constants. This applies to sl and sh to be the 29 Structural Bit-Vector Model Counting Kim and McCamant ( bvadd f g ) if isConstant ( f ) and isConstant ( g ): ul = uh = ( f . ul + g . ul ) % 2^ f . width sl = sh = ( f . sl + g . sl ) % 2^ f . width return ul , uh , sl , sh , 1 , 1 , true , [ f . vars ∪ g . vars ] if f . uh + g . uh > umax : ul = umin uh = umax else : ul = f . ul + g . ul uh = f . uh + g . uh if f . sl + g . sl < smin or f . sh + g . sh > smax : sl = smin sh = smax else : sl = f . sl + g . sl sh = f . sh + g . sh lc = min ( f . lc + g . lc -1 , abs ( uh - ul ) , abs ( sh - sl )) if isCommon (f , g ): lc = 1 hc = min ( f . hc * g . hc , abs ( uh - ul ) , abs ( sh - sl )) hom = ( f . hom and isConstant ( g )) or ( isConstant ( f ) and g . hom ) or ( not isCommon (f , g ) and isPerm ( f ) and isPerm ( g )) return ul , uh , sl , sh , lc , hc , hom , [ f . vars ∪ g . vars ] Figure 2: The operation rule of bvadd negative minimum and positive maximum. lc and hc can be computed as the sum of two variable’s minimum cardinality minus 1. In order to generate the smallest set of adding two sets, one value has to be generated in multiple ways. For example, adding {1, 2, 3} and {2, 3} makes {3, 4, 5, 6} which has 4 elements. If the function has variables in common (for example, (x&1)+(¬x&1)), the minimum cardinality could be 1. The maximum cardinality can be computed as the multiplication of each variable’s maximum cardinality. Note that the cardinalities must be less than the distance between its high value and low value. The addition is homogeneous if one variable is homogeneous and another is a constant or they do not have variables in common and both are permutations. A variable is a permutation if it is homogeneous and unconstrained. Let us go back to the example in Fig 1 and proceed with the SMC algorithm. When x and y are declared, two corresponding nodes are generated. Initial values of x would be [0, 255, -128, 127, 256, 256, true, {x}] and initial values of y would be the same except vars={y}. If we have the equation (= y (bvadd (bvand x 15) 4)), we parse the equation and generate a node from the expression. (bvand x 15) returns a node with 30 Structural Bit-Vector Model Counting Kim and McCamant (= f g ) ··· leq = max ( f . ul , g . ul ) heq = min ( f . uh , g . uh ) minlhit = f . lc - max ( f . uh - heq , leq - f . ul ) minlhit = min ( minlhit , heq - leq + 1) minrhit = g . lc - max ( g . uh - heq , leq - g . ul ) minrhit = min ( minrhit , heq - leq + 1) inter = max (1 , minlhit + minrhit - ( heq - leq + 1)) ic = 2^( f . width + g . width ) if f . hom : ld_f = 2^ f . width / f . hc hd_f = 2^ f . width / f . lc else : ld_f = 1 hd_f = 2^ f . width - f . lc + 1 if g . hom : ld_g = 2^ g . width / g . hc hd_g = 2^ g . width / g . lc else : ld_g = 1 hd_g = 2^ g . width - g . lc + 1 lb = max (1 , min ( inter * ld_f * ld_g , ic )) hb = min ( inter * hd_f * hd_g , ic ) ··· Figure 3: The operation rule of = [0, 15, 0, 15, 16, 16, true, {x}] and then (bvadd (bvand x 15) 4) returns a node with [4, 19, 4, 19, 16, 16, true, {x}]. When there is an equality or inequality check in an as- sertion, SMC computes a lower bounds and upper bound of variables in the assertion. We denote lb and hb which are the lower and upper bounds of a set of variables, respectively. Fig 3 shows the crucial part to compute the bounds. This equal rule computes the cardinalities of the left-hand side and the right-hand side and then the cardinality of the intersection between the left-hand side and the right-hand. Depending on the homogeneity of the variable, we compute the low and high density of the variable so we can compute the lower bound and upper bound. We also apply the same procedure to signed values and select the bounds that has a smaller interval. In this example, SMC computes the lower bound as 256 and the upper bound as 256, which is an accurate answer. 3.1.2 Combining Bounds The second step is to combine per-assertion bounds. For each assertion with comparison op- erators such as equal, greater-than or less-than, we compute the lower and upper bounds on the number of solutions to variables in the assertion. Recall that lb and hb are the bounds of a set of variables. We use vars to denote the set of variables in an assertion. Given two 31 Structural Bit-Vector Model Counting Kim and McCamant mergeBounds ( Bounds a , Bounds b ): vars = a . vars ∪ b . vars inter_vars = a . vars ∩ b . vars width = inter_vars . width inter_max = min (2^ width , math . gcd ( a . ha , b . ha )) inter_min = min (2^ width , math . gcd ( a . la , b . la )) if a . vars and b . vars are in common : if set ( a . vars ) == set ( b . vars ): la = min ( a . la , b . la ) ha = min ( a . ha , b . ha ) elif a . vars ⊂ b . vars : la = b . la ha = b . ha elif b . vars ⊂ a . vars : la = a . la ha = a . ha else : ula = a . ula * b . ula / inter_min uha = a . uha * b . uha / inter_max else : la = a . la * b . la ha = a . ha * b . ha return Bounds ( la , ha , vars ) Figure 4: The operation rule of mergeBounds such bounds, we can merge per-assertion bounds into bounds that apply to both equations together. We recursively merge the bounds pairwise until the bound represent all the variables in the system. For example, if two bounds are independent, we can simply multiply each lower bound and upper bound. We present pseudocode for merging bounds in Figure 4. We first check whether two bounds are independent or not. If they are independent, we can just simply multiply two bounds. If they have variables in common, then we consider four cases: they are identical, one is subset of another (or vice versa) and they are overlapping sets. We compute the bounds conservatively based on the case. The bounds can be more precise based on the order of merging such as merging similar variables first. This needs an extra running time and we left this for the future work. 3.2 Differences between SMC and FSCB Here we briefly describe the differences between SMC and FSCB. First, we cover a more com- plete set of bit-vector operators for both the signed and unsigned orderings of bit vectors. Table 1 shows which bit-vector operators are supported by FSCB and SMC. Also, we added more edge cases in operators and fixed some operators to compute a better precision. For example, bvadd in FSCB computes the low cardinality as max(f.lc, g.lc) but we empirically find out that f.lc+g.lc-1 gives a better result. 32 Structural Bit-Vector Model Counting Kim and McCamant FSCB bvadd, bvsub, bvmul, bvand, bvor, bvxor, bvshl, bvlshr, =, distinct, ult, ugt SMC bvadd, bvsub, bvmul, bvand, bvor, bvxor, bvshl, bvlshr, =, distinct, ult, ugt, ule, uge, slt, sgt, sle, sge, bvudiv, bvsdiv, concat, extract, sign extend Table 1: Bit-vector operators supported by SMC and FSCB 3.3 Correctness We have tested the correctness of the operation rules of bit-vector expression using bounded exhaustive checking. We set each variable to be a bit-vector of width 4 and executed each operator with the power set of each variable. We checked whether ul, uh, sl, sh, lc and hc from our operation rules are sound. We verify unary operators and binary operators. First, we compute ul, uh, sl, sh, lc and hc based on our operation rules. We generate the power set of one variable which has 216 sets and execute an operation which generates 232 sets for binary operators. The same procedure is applied to unary operators. We verify that (1)the unsigned smallest value of each set is greater than ul, (2)the unsigned largest value of each set is less than uh, (3)the signed smallest value of each set is greater than sl, (4)the signed largest value of each set is less than sh and (5)the number of elements of each set is less than hc and greater than lc. However, we have not checked the correctness of merging bounds due to the state explosion problem since we need to test the case where bounds contain multiple variables. 3.4 Limitation In this section, we discuss the limitations of our current implementation. We have extended FSCB to support more operators in SMT-LIB2 format. However, some of SMT-LIB2 operators are not supported in SMC and we are currently working on handling the whole SMT-LIB2 format standard. Also, some operators compute the cardinalities very conservatively due to the limitation of the node representation, hence those operators lead to less precise results (loose bounds). This is for the future work to have more coverage of SMT-LIB2 format standard and design more precise rules. Lastly, the order of assertions and merging bounds affects precision. For example, let say we have two variable v1 and v2 and one constant c. If we have assertions (= v1 v2 ) and (= v2 c), the results are computed differently depending on which assertion is processed first. For example, (= v1 v2 ) computes the bounds [256, 256] and (= v2 c) computes the bounds [1, 1] if all the variables are 8-bit. If we merge the two bounds, the final bound would be [256, 256]. But if we flip the order which (= v2 c) computes the bounds first, then (= v1 v2 ) computes the bounds [1, 1] since we know that v2 is a constant value this time. This can be resolved by recursively computing the bounds until the bounds do not change but we do not have any proof about its time complexity. This means the bounds can be more precise by merging the per-assertion bounds in a better order. We believe finding more efficient way to merge bounds will improve the performance and this is for the future work. 4 Experimental Results In this section, we show our experimental results and all our experiments were performed on a machine with an Intel Core i7 3.40Ghz CPU and 16GB memory. We implement our algorithm with Python and use our own SMT-LIB2 parser. Our algorithm supports SMT-LIB2 format [3]. We compare our algorithm with state-of-the-art model counters: SearchMC [13] and 33 Structural Bit-Vector Model Counting Kim and McCamant dSharp p [2]. SearchMC is an approximate model counter using XOR hashing constraints to estimate a lower bound and upper bound of the model count. It is a randomized algorithm and gives a desired level of distance between a lower bound and upper bound with a probability of at least 0.6. In this experiment, we ran SearchMC 10 times for each benchmark until it gave the first bounds with a probability of at least 0.6 and computed the average of the results. dSharp p is an exact model counter and is implemented on top of dSharp [18] to support projection. We collected various SMT BV benchmarks from previous works [10, 11]. Here we show partial results of some representative benchmarks. Table 2 shows a comparison on performance and approximation. The second column shows the number of bits we want to count over. Since dSharp p is an exact model counter, we take log2 of the answer which shows in the third column and the running times (in seconds) of dSharp p are shown in the fourth column. We also show the bounds (log base 2) computed from SearchMC and SMC following with their running times. dSharp p performs well on a small-sized problems and its performance decreases as the size and the complexity of formula increases. In these experiments, SearchMC used the state-of-the-art SMT(BV) solver Z3 [9] and its performance was highly dependent on the performance of the solver. SMC shows a good precision on some benchmarks if the structure of the formula is well- organized. However, it gave very loose bounds on some benchmarks which SMC was not able to analyze the formula well. For example, 5 10 1 and 5 20 1 are the volume computation problems of convex bodies and consist of a number of inequality constraints. This type of problems show very loose bounds since SMC computes the bounds very conservatively on inequality constraints. The main benefit of SMC is the running times. This shows that our approach is faster than others and it is a trade-off chosen between computational effort and the precision of results in some benchmarks. Hashing-based model counting techniques like SearchMC rely on prior hypotheses to produce more useful results and start an initial hypothesis from zero knowledge. The initial hypothesis for SearchMC is a uniform distribution over 0 to the maximum bit-width of the output bit- vector. If we gather results from SMC and use them as the initial hypothesis for SearchMC, SearchMC is able to give a desired answer faster. For example, in order to solve coloring 4 the initial hypothesis for SearchMC is a uniform distribution over 0 to 32. If the initial hypothesis for SearchMC is a uniform distribution over 29.61 to 32 which is computed by SMC, SearchMC needs a smaller number of queries to find a desired result. Table 3 shows the performance of the combination of SMC and SearchMC. The results for plain SearchMC are equivalent to the results in Table 2. We also measured the average number of iterations (loops) in SearchMC and the results show that the number of iterations was decreased when we used SMC and SearchMC together. Since SMC already computed tight bounds on gettoPath1 and calDate 10, we did not run SearchMC on the benchmarks. This experimental results show that using SMC as a preprocessor of SearchMC gives the performance benefit up to 1.36x speedup. 5 Conclusion We propose a structural approximate model counting algorithm, SMC, to compute the lower and upper bound of solutions to a given SMT formula. This is a fast polynomial algorithm compared to other state-of-the-art approximate model counters and it runs in O(n + m) where n is the number of variables and m is the number of assertions. We extend the FSCB algorithm to cover a more complete set of SMT-LIB2 standard operators and to use both the signed and unsigned representations of bit vectors. Our evaluation results illustrate that our technique is 34 Structural Bit-Vector Model Counting Kim and McCamant dSharp p SearchMC SMC Benchmarks #Bits log2 (M C) t(s) Bounds t(s) Bounds t(s) coloring 4 32 30.75 0.82 [30.15 31.05] 1088.52 [29.61 32.00] 0.001 FINDpath1 32 21.96 0.09 [20.9 22.17] 3.99 [4.00 32.00] 0.001 getopPath1 8 7.92 0.003 [7.50 8.25] 0.21 [7.92 7.94] 0.001 queue 16 6.39 0.006 [5.66 6.97] 0.17 [4.62 10.78] 0.001 calDate 10 36 16.95 0.002 [16.13 17.49] 0.30 [16.95 16.95] 0.001 5 10 1 160 12.02 123.12 [11.34 12.31] 20.73 [7.24 24.77] 0.003 5 20 1 160 8.44 351.57 [7.691 8.88] 29.6 [7.24 24.77] 0.004 Table 2: Comparison Result SearchMC SMC+SearchMC Benchmarks #Bits Bounds t(s) #loops Bounds t(s) #loops coloring 4 32 [30.15 31.05] 1088.52 6.3 [30.16 31.53] 830.88 4.9 FINDpath1 32 [20.9 22.17] 3.99 8.2 [21.24 22.42] 3.55 7.7 getopPath1 8 [7.50 8.25] 0.21 4 - - - queue 16 [5.66 6.97] 0.17 6.1 [5.60 6.78] 0.15 4.8 calDate 10 36 [16.13 17.49] 0.30 8.3 - - - 5 10 1 160 [11.34 12.31] 20.73 8.9 [11.2 12.44] 18.3 6.4 5 20 1 160 [7.691 8.88] 29.62 8.4 [7.42 8.85] 21.83 5.3 Table 3: Combination of SMC and SearchMC most beneficial when time performance is a tight requirement. Acknowledgments We would like to thank the anonymous reviewers for suggestions which have helped us to improve our system and the paper’s presentation. The research described in this paper has been supported in part by the National Science Foundation under grant 1526319 and by the Office of Naval Research under grant N00014-19-1-2541. References [1] Abdulbaki Aydin, William Eiers, Lucas Bang, Tegan Brennan, Miroslav Gavrilov, Tevfik Bultan, and Fang Yu. Parameterized model counting for string and numeric constraints. In Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, November 04-09, 2018, pages 400–410, 2018. [2] Rehan Abdul Aziz, Geoffrey Chu, Christian Muise, and Peter Stuckey. #∃SAT: Projected model counting. In Theory and Applications of Satisfiability Testing, 2015. [3] Clark Barrett, Aaron Stump, and Cesare Tinelli. The SMT-LIB standard: Version 2.0. Technical report, Department of Computer Science, The University of Iowa, 2010. [4] Roberto J. Bayardo, Jr. and Robert C. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of AAAI, pages 203–208, 1997. [5] Jan Burchard, Tobias Schubert, and Bernd Becker. Laissez-Faire caching for parallel #SAT solving. In Proceedings of SAT, pages 46–61, 2015. 35 Structural Bit-Vector Model Counting Kim and McCamant [6] Miguel Castro, Manuel Costa, and Jean-Philippe Martin. Better bug reporting with better privacy. In Proceedings of ASPLOS, pages 319–328, 2008. [7] Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. A scalable approximate model counter. In Proceedings of CP, volume 8124, pages 200–216, 2013. [8] Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. Improving approximate counting for probabilistic inference: From linear to logarithmic SAT solver calls. In Proceedings of IJCAI, pages 3569–3576, 2016. [9] Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In Proceedings of TACAS, pages 337–340, 2008. [10] Wei Gao, Hengyi Lv, Qiang Zhang, and Dunbo Cai. Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method. Algorithms, 11:142, 2018. [11] Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, and Xutong Ma. A new probabilistic algorithm for approximate model counting. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning, 2018. [12] Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting: A new strategy for obtain- ing good bounds. In Proceedings, The Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, July 16-20, 2006, Boston, Massachusetts, USA, pages 54–61, 2006. [13] Seonmo Kim and Stephen McCamant. Bit-vector model counting using statistical estimation. In Tools and Algorithms for the Construction and Analysis of Systems, 2018. [14] Vladimir Klebanov, Alexander Weigl, and Jörg Weisbarth. Sound Probabilistic #SAT with Pro- jection. In Workshop on QAPL, 2016. [15] Loi Luu, Shweta Shinde, Prateek Saxena, and Brian Demsky. A model counter for constraints over unbounded strings. In Proceedings of PLDI, pages 565–576, 2014. [16] Jean-Philippe Martin. Upper and lower bounds on the number of solutions. Technical Report MSR-TR-2007-164, Microsoft Research, 2007. [17] Ziyuan Meng and Geoffrey Smith. Calculating bounds on information leakage using two-bit pat- terns. In Proceedings of PLAS, pages 1:1–1:12, 2011. [18] Christian Muise, Sheila A. McIlraith, J. Christopher Beck, and Eric Hsu. DSHARP: Fast d-DNNF Compilation with sharpSAT. In Canadian Conf. on Artificial Intelligence, 2012. [19] Tian Sang, Fahiem Bacchus, Paul Beame, Henry A. Kautz, and Toniann Pitassi. Combining component caching and clause learning for effective model counting. In Proceedings of SAT, 2004. [20] Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilis- tic exact model counter. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 1169–1176. ijcai.org, 2019. [21] Michael Sipser. A complexity theoretic approach to randomness. In Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, page 330–335, 1983. [22] Mate Soos and Kuldeep Meel. Bird: Engineering an efficient cnf-xor sat solver and its applications to approximate model counting. Proceedings of the AAAI Conference on Artificial Intelligence, 2019. [23] Larry Stockmeyer. The complexity of approximate counting. In Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, page 118–126, 1983. [24] Marc Thurley. sharpSAT - counting models with advanced component caching and implicit BCP. In Proceedings of SAT, pages 424–429, 2006. [25] Leslie G. Valiant and Vijay V. Vazirani. NP is as easy as detecting unique solutions. Theor. Comput. Sci., 47(3):85–93, 1986. 36