# 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
As can be seen from the bottom row in Table 6, over the ten instances (5-10-1, 5-10-2, 5-10-4, 5-10-5, 5-20-1, 5-20-2, 5-20-3, 5-20-4, 5-20-5, 6-10-1) on which all the three methods return none-zero results, the averaged time costs of MCMC-Flat\({}^{1/2}\), SMTApproxMC, and ApproxMC2 are 344.5, 955.80, and 463.33, respectively. Obviously, MCMC-Flat\({}^{1/2}\) is the fastest. \begin{table}
\begin{tabular}{c c c c c c c c c c} \hline \multirow{2}{*}{**Prob.**} & \multicolumn{3}{c}{**MCMC-Flat\({}^{1/2}\)**} & \multicolumn{3}{c}{**SMTAApproxMC**} & \multicolumn{3}{c}{**ApproxMC2**} \\ \cline{2-10}  & **Vol.** & **Time** & **RE (\%)** & **Vol.** & **Time** & **RE (\%)** & **Vol.** & **Time** & **RE (\%)** \\ \hline
5-10-1 & 4394.4 & 625.51 & **5.6** & 16 & 504.15 & \(-\)99.6 & 4416 & 28.37 & 6.1 \\
5-10-2 & 7319.1 & 60.11 & 52.1 & 19.5 & 552.85 & \(-\)99.6 & 4608 & 34.99 & \(-\)**4.3** \\
5-10-3 & \(1.94\times 10^{5}\) & 9.73 & **19.0** & \(1.97\times 10^{5}\) & 2158.77 & 20.3 & 0 & \(4.20\times 10^{3}\) & \(-\)100 \\
5-10-4 & 13169.6 & 16.34 & 11.2 & 45 & 1276.02 & \(-\)99.6 & 12,288 & 104.77 & **3.7** \\
5-10-5 & \(2.43\times 10^{5}\) & 56.09 & **2.1** & 3 & 1570.6 & \(-\)100 & \(2.21\times 10^{5}\) & \(2.43\times 10^{3}\) & \(-\)7.2 \\
5-20-1 & 347.5 & 75.47 & **0.1** & 21 & 562.4 & \(-\)93.9 & 352 & 24.6 & 1.4 \\
5-20-2 & 260.4 & 1555.6 & 5.0 & 239 & 489.37 & \(-\)3.6 & 248 & 22.75 & **0.0** \\
5-20-3 & 898.3 & 91.32 & \(-\)**16.8** & 833 & 545.84 & \(-\)22.9 & 880 & 28.13 & \(-\)18.5 \\
5-20-4 & 7.9 & 162.1 & -1.3 & 2.5 & 85.53 & \(-\)68.8 & 8 & 28.94 & **0.0** \\
5-20-5 & 17.8 & 719.27 & 48.3 & 3.5 & 310.64 & \(-\)70.8 & 12 & 1.55 & **0.0** \\
6-5-1 & \(1.74\times 10^{6}\) & 28.67 & \(-\)**6.2** & \(\backslash\) & & \(\backslash\) & 0 & \(5.74\times 10^{3}\) & \(-\)100 \\
6-5-2 & \(6.52\times 10^{6}\) & 5.7 & \(-\)**14.2** & \(2.56\times 10^{6}\) & 56,611.85 & \(-\)66.4 & 0 & \(6.00\times 10^{3}\) & \(-\)100 \\
6-5-3 & \(5.37\times 10^{6}\) & \(\backslash\) & 796.73 & 79.5 & 52,437.11 & \(\backslash\) & 0 & \(6.00\times 10^{3}\) & \(\backslash\) \\
6-5-4 & \(9.43\times 10^{6}\) & 5.62 & \(-\)**25.2** & 192.5 & 65,540.31 & \(-\)100 & 0 & \(6.00\times 10^{3}\) & \(-\)100 \\
6-5-5 & \(7.45\times 10^{6}\) & 9.71 & \(\backslash\) & \(1.04\times 10^{7}\) & 68,279.69 & \(\backslash\) & 0 & \(6.00\times 10^{3}\) & \(\backslash\) \\
6-10-1 & \(1.48\times 10^{5}\) & 83.67 & \(\backslash\) & \(1.31\times 10^{5}\) & 3660.63 & \(\backslash\) & \(1.19\times 10^{5}\) & \(1.93\times 10^{3}\) & \(\backslash\) \\
7-5-1 & \(4.91\times 10^{8}\) & 21.86 & \(\backslash\) & \(\backslash\) & \(\backslash\) & \(\backslash\) & 0 & \(5.29\times 10^{3}\) & \(\backslash\) \\
7-5-2 & \(1.41\times 10^{8}\) & 9.31 & \(\backslash\) & \(\backslash\) & \(\backslash\) & \(\backslash\) & 0 & \(6.00\times 10^{3}\) & \(\backslash\) \\
7-5-3 & \(7.00\times 10^{8}\) & 25.09 & \(\backslash\) & \(\backslash\) & \(\backslash\) & \(\backslash\) & 0 & \(6.00\times 10^{3}\) & \(\backslash\) \\
7-5-4 & \(6.58\times 10^{8}\) & 8.23 & \(\backslash\) & \(\backslash\) & \(\backslash\) & \(\backslash\) & 0 & \(6.00\times 10^{3}\) & \(\backslash\) \\
7-5-5 & \(1.65\times 10^{8}\) & 14.54 & \(\backslash\) & \(\backslash\) & \(\backslash\) & \(\backslash\) & 0 & \(6.00\times 10^{3}\) & \(\backslash\) \\
7-10-1 & \(6.58\times 10^{4}\) & 634.31 & \(\backslash\) & \(\backslash\) & \(\backslash\) & \(\backslash\) & \(5.63\times 10^{4}\) & \(1.15\times 10^{3}\) & \(\backslash\) \\ \hline \#Solved & **22** & & & 15 & & & 11 & \\ \#BestRE & **8** & & 0 & & & 5 & & \\ AvgTime & **344.55** & & 955.80 & & & 463.33 & & \\ \hline \end{tabular}
\end{table} 
Table 6: Comparison of MCMC-Flat\({}^{1/2}\), SMTApproxMC and ApproxMC2 on convex bodies. * Regarding the ability of obtaining samples from the solution area for large size instances, MCMC-Flat\({}^{1/2}\) is superior to the direct Mont Carlo method in [24].