# Estimating the Volume of the Solution Space of SMT(LIA) Constraints by a Flat Histogram Method
## 3 Related Works  
A pioneer work of applying the flat histogram method in model counting is for Boolean formulas [22]. The authors built the connection between the model counting problem of SAT and the DOS computation problem. Their method was shown to outperform the standard Metropolis sampling. In this work, we extend the flat histogram to the field of SMT for solving #SMT(LIA). A recent work on #SMT(LIA) developed a multiphase Monte-Carlo method that exploits a novel technique for estimating the volume of convex polytopes [9]. Specifically, that work designed a set of strategies to reduce the number of samplings. On top of their methods, a tool called VolCE that uses LattE [23] was developed (we refer to it as VolCE+LattE) for #SMT(LIA). Experiments in [9] show that VolCE+LattE is superior to a word-level hash-mapping method SMTApproxMC [19] on instances which have more than 4,000,000 solutions. Hash-mapping-based approximate methods for model counting of SMT formulas have been paid much attention in recent years. The bit-level hash-mapping-based methods ApproxMC [20] and its improved version ApproxMC2 [21] used XOR-based bit-level hash functions to obtain a randomized subset of the solution space by calling a satisfiability solver. However, the approaches have the danger of introducing too many discrete variables when dealing with linear real constraints [9]. On the other hand, meanings of variables are lost in a bit-level encoding, as argued in [9; 19]. To advance the techniques of estimating by hash-mapping and to overcome the weakness of bit-level encoding, a word-level hash-mapping method was proposed in [19], where an approximate model counter for linear integer constraints called SMTApproxMC was developed. A great advantage of SMTApproxMC is the ability to exploits the continuously advanced reasoning power of word-level SMT solvers. However, SMTApproxMC is reported to have difficulty in scaling to instances having a large number of solutions [9]. Monte-Carlo based model counting (or volume computation) has a wealth of studies. Nonetheless, few implementations are available for SMT. One recently implemented direct Monte-Carlo method for SMT with linear real constraints was reported in [24]. They showed, by experiments on a set of convex bodies involving increasing number of variables, their direct Monte Carlo method fails on all instances with seven or more variables. In contrast, our experiments (in Section 5: More Results on Convex Bodies) on a subset of their benchmarks will show that one of our techniques can work on many instances with seven or more variables. We briefly summarize the characteristics of our techniques and the related as follows. * Our techniques vs. VolCE+LattE [9]: Both techniques are suited for #SMT(LIA). VolCE+LattE is an exact method whereas our methods are approximate. In our experiments, VolCE+LattE fails to scale on many convex body instances (obtained from [24]) that are with more than six variables, whereas one of our techniques succeed in reporting solutions for the test set. Note that both techniques require low memories. In our test, their required memory on all instances is less than 1 GB. So, a failure of VolCE+LattE is due to time out. * Our techniques vs. SMTApproxMC [19] and ApproxMC2 [21]: The three are approximate techniques. SMTApproxMC and ApproxMC2 provide a guarantee that if given a tolerance \(\varepsilon>\)0 and a confidence 1-\(\delta\in(0,1)\), its output lies in the interval \([(1+\varepsilon)^{-1}\)\(\mathrm{R_{F}}\), \((1+\varepsilon)\)\(\mathrm{R_{F}}\)] with probability greater than \(\delta\), where \(\mathrm{R_{F}}\) is the real count of a formula. Our techniques do not provide such a guarantee. However, experiments will show that our techniques lead to a relative error smaller than 20% in most of the tests. In addition, our methods are capable of working on tested instances with 4,000,000 and more solutions, whereas SMTApproxMC cannot. ApproxMC2 has similar scalability issue as well (see Section 5: More Results on Convex Bodies).