# Estimating the Volume of the Solution Space of SMT(LIA) Constraints by a Flat Histogram Method
## 4 The Proposed Flat Histogram Method
### The Sampling Algorithm
For SMTApproxMC, equations in the form of (8) are translated into sentences in the Fixed Size Bit Vector theory of SMT-LIB2, where the size of a bit vector is 32. To run ApproxMC2 [21], the benchmark problems were bit-blasted by using an embedded function of the SMT solver Yices ([[http://yices.csl.sri.com/](http://yices.csl.sri.com/)]([http://yices.csl.sri.com/](http://yices.csl.sri.com/))). Specifically, for the problems described in the SMT-LIB2 Bit Vector theory (which is suited for SMTApproxMC), the SMT-LIB2 keywords are replaced by Yices' corresponding ones, for example: \"bvsle\" in SMT-LIB2 is replaced with \"bv-sle\" in the Yices language. Furthermore, at the end of the problem, an \"export-to-dimacs\" command is set. The resulted problem file was then bit-blasted by Yices (with command-line option \"-logic = QF_BV\"). \begin{table}
\begin{tabular}{c c c c c} \hline \hline
**Problems** & **\#Variable** & **\#Constraint** & **Space** & **Volume/Space (\%)** \\ \hline



\hline \hline \end{tabular}
\end{table} 
Table 4: Properties of problems used to compare MCMC-Flat\({}^{1/2}\), Volce+LattE, and SMTApproxMC. All the original and translated problems for SMTApproxMC and ApproxMC2 are publicly available ([[https://github.com/PlanningByCai/MCMCFlat-Count-1-2](https://github.com/PlanningByCai/MCMCFlat-Count-1-2)]([https://github.com/PlanningByCai/MCMCFlat-Count-1-2](https://github.com/PlanningByCai/MCMCFlat-Count-1-2))). This part of the test was carried out on a 64-bit Linux platform with a 2.6 GHz CPU, 4 GB memory limit. The time limit of each test is 12 h. Volce+LattE was executed once, since it is an exact method. MCMC-Flat\({}^{1/2}\) was given 5 runs on each instance and the averaged results are reported. A \"\(\backslash\)\" indicates failure due to time out. SMTApproxMC was run with the default configuration (50 iterations, tolerance \(\varepsilon\) = 0.8 and \(\delta\) = 0.2, for an instance). Note that these settings for \(\varepsilon\) and \(\delta\) are the same as those used by the authors of SMTApproxMC, which make the value \(v\) returned by SMTApproxMC satisfy

\[\Pr\left[\frac{|R_{F}|}{1+\varepsilon}<v<(1+\varepsilon)|R_{F}|\right]\geq 1-\delta \tag{9}\]

Note that RF is the real volume. ApproxMC2 was run with its default configuration as well (with the same \(\varepsilon\) and \(\delta\)). So, return values of ApproxMC2 satisfy (9) as well. Results regarding Volce+LattE and MCMC-Flat\({}^{1/2}\) are shown in Table 5. We can observe that Volce+LattE fails on many instances with 6 and 7 variables, among which it only succeeds on 6-5-1, 6-5-2, and 6-5-4 with dozens of minutes. In contrast, our MCMC-Flat\({}^{1/2}\) method works on all the instances. On the other hand, MCMC-Flat\({}^{1/2}\) reports a result of 1.74 \(\times\) 10\({}^{8}\) on the problem 6-5-1 with a relative error 6.21%. In summary, on the 13 instances on which Volce+LattE succeeds, MCMC-Flat\({}^{1/2}\) gives 3 results with RE beyond 20% (52.07% for 5-10-2, 48.17% for 5-20-5, and \(-25.17\%\) for 6-5-4), and gives the other 10 results with RE in [\(-20\%\), \(20\%\)]. Therefore, results in Table 5 show that MCMC-Flat\({}^{1/2}\) is more scalable than Volce+LattE. Table 6 are results of MCMC-Flat\({}^{1/2}\), SMTApproxMC and ApproxMC2; the results of MCMC-Flat\({}^{1/2}\) are the same as those in Table 5. In Table 6, a brief summary of the results is presented at the bottom: \"#Solved\" is the number of solved instances of an algorithm, \"#BestRE\" is the number of instances on which an algorithm obtained the best relative error, and \"#AvgTime\" is the averaged solving time over instances that are solved by all the three algorithms.