# 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
\begin{table}
\begin{tabular}{l c c c c c} \hline \hline \multirow{2}{*}{**Prob**} & \multicolumn{2}{c}{**Volce+LattE**} & \multicolumn{2}{c}{**MCMC-Flat\({}^{1/2}\)**} \\ \cline{2-6}  & **Vol.** & **Time** & **Vol.** & **Time** & **RE (\%)** \\ \hline
5-10-1 & 4162 & 13.5 & 4394.4 & 625.51 & 5.6 \\
5-10-2 & 4813 & 111.43 & 7319.1 & 60.11 & 52.1 \\
5-10-3 & \(1.63\times 10^{5}\) & 218.25 & \(1.94\times 10^{5}\) & 9.73 & 19.0 \\
5-10-4 & 11844 & 302.69 & 13169.6 & 16.34 & 11.2 \\
5-10-5 & \(2.38\times 10^{5}\) & 95.22 & \(2.43\times 10^{5}\) & 56.09 & 2.1 \\
5-20-1 & 347 & 383.69 & 347.5 & 75.47 & 0.1 \\
5-20-2 & 248 & 366.6 & 260.4 & 1555.6 & 5.0 \\
5-20-3 & 1080 & 194.86 & 898.3 & 91.32 & \(-16.8\) \\
5-20-4 & 8 & 257.82 & 7.9 & 162.1 & \(-1.3\) \\
5-20-5 & 12 & 643.42 & 17.8 & 719.27 & 48.3 \\
6-5-1 & \(1.85\times 10^{8}\) & 2248.59 & \(1.74\times 10^{8}\) & 28.67 & \(-6.2\) \\
6-5-2 & \(7.60\times 10^{6}\) & 1059.29 & \(6.52\times 10^{6}\) & 5.7 & \(-14.2\) \\
6-5-3 & \(\backslash\) & \(\backslash\) & \(5.37\times 10^{6}\) & 796.73 & \(\backslash\) \\
6-5-4 & \(1.26\times 10^{7}\) & 839.3 & \(9.43\times 10^{6}\) & 5.62 & \(-25.2\) \\
6-5-5 & \(\backslash\) & \(\backslash\) & \(7.45\times 10^{6}\) & 9.71 & \(\backslash\) \\
6-10-1 & \(\backslash\) & \(\backslash\) & \(1.48\times 10^{5}\) & 83.67 & \(\backslash\) \\
7-5-1 & \(\backslash\) & \(\backslash\) & \(4.91\times 10^{8}\) & 21.86 & \(\backslash\) \\
7-5-2 & \(\backslash\) & \(\backslash\) & \(1.41\times 10^{8}\) & 9.31 & \(\backslash\) \\
7-5-3 & \(\backslash\) & \(\backslash\) & \(7.00\times 10^{8}\) & 25.09 & \(\backslash\) \\
7-5-4 & \(\backslash\) & \(\backslash\) & \(6.58\times 10^{8}\) & 8.23 & \(\backslash\) \\
7-5-5 & \(\backslash\) & \(\backslash\) & \(1.65\times 10^{8}\) & 14.54 & \(\backslash\) \\
7-10-1 & \(\backslash\) & \(\backslash\) & \(6.58\times 10^{4}\) & 634.31 & \(\backslash\) \\ \hline \hline \end{tabular}
\end{table} 
Table 5: Comparison of Volce+LattE and MCMC-Flat\({}^{1/2}\) on convex bodies. We make several observations from the results in Table 6, as follows. * In terms of scalability, our MCMC-Flat\({}^{1/2}\) method is superior to SMTApproxMC and ApproxMC2. In [9], the word-level hash-mapping-based method SMTApproxMC was shown to handle instances with less than 3.98 \(\times\) 10\({}^{6}\) models (around 4,000,000) and failed on others. On our test platform, SMTApproxMC got a result of 1.04 \(\times\) 10\({}^{7}\) on instance 6-5-5. However, SMTApproxMC can return a value 15 out of 22 instances, whereas MCMC-Flat\({}^{1/2}\) returns values on all the 22 instances. Notably, MCMC-Flat\({}^{1/2}\) reports a result of 1.74 \(\times\) 10\({}^{8}\) on the problem 6-5-1 with a low relative error 6.21%. From the results, the scalability of SMTApproxMC is better than ApproxMC2, as the former solved 15 instances whereas the latter solved 11 instances. Therefore, MCMC-Flat\({}^{1/2}\) is the best, with respect to scalability. * In terms of accuracy, MCMC-Flat\({}^{1/2}\) is better than SMTApproxMC and ApproxMC2. Among 13 instances for which the exact volume is known by Volce+LattE (see Table 5), MCMC-Flat\({}^{1/2}\) returns best results on 8 instances, and ApproxMC2 does the best on the other 5 instances, in terms of relative error. The accuracy of SMTApproxMC is not competitive to either MCMC-Flat\({}^{1/2}\) or ApproxMC2. The variance in relative errors of ApproxMC2 is better than that of MCMC-Flat\({}^{1/2}\), as we can observe from Table 6 that on instances where ApproxMC2 returns none-zero results the relative error of ApproxMC2 is better than that of MCMC-Flat\({}^{1/2}\). On the other hand, ApproxMC2 seems to have big difficulty in working on instances having volume greater than 1.0 \(\times\) 10\({}^{6}\), as it takes relatively long time on instances 5-10-1, 6-10-1, and 7-10-1. * In terms of efficiency, MCMC-Flat\({}^{1/2}\) is significantly better than SMTApproxMC and ApproxMC2.