# 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
The programs were restricted to run on one core of the CPU by using the Linux command taskset. MCMC-Flat\({}^{1/2}\) and MCMC-Flat\({}^{1/t\text{-pv}}\) were run 10 times on each problem; their results were averaged on successful runs. In the following results, Vol. is short for volume, SR is short for success ratio, and RE is short for relative error. Let \(d^{\prime}\) be an estimation of a target value \(d\), we define the relative error \(d\) to \(d^{\prime}\) as \(\text{RE}(d,\,d^{\prime})=(d^{\prime}-d)/d\). We use MO to indicate the memory out of the Exact Method and use \"\(\backslash\)\" to indicate 'time out'. With structural instances, we want to see that whether the accuracies of MCMC-Flat methods improve with increasing size of volumes. The detailed results are shown in Table 2. On instance \(s1\), the relative errors of MCMC-Flat\({}^{1/2}\) and MCMC-Flat\({}^{1/t\text{-pv}}\) are 302.69% and 297.97%, respectively. The errors of the two algorithms decrease consistently when the volumes of the target convex bodies increase. In addition, on the structured instance \(s6\) which is with the maximal volume 4096, both of our algorithms reach small relative errors within 10% (9.33% and 5.65% for MCMC-Flat\({}^{1/2}\) and MCMC-Flat\({}^{1/t\text{-pv}}\), respectively). We can also see that MCMC-Flat\({}^{1/t-\text{pv}}\) leads to smaller relative errors, compared with MCMC-Flat\({}^{1/2}\), on instances \(s5\), \(s6\) and \(s7\), though the running times of the former are more than the latter. Finally, we note that the Exact Method is the fastest among these three algorithms, with nearly neglectable running times. However, this advantage of the Exact Method will be lost on complex SMT(LIA) formulas contained in our random instances. With random instances, the ability of MCMC-Flat methods on hard instances is verified (see Table 3). Table 3 shows that MCMC-Flat\({}^{1/t\text{-pv}}\) reaches good accuracy very fast, in contrast with \begin{table}
\begin{tabular}{c c c c} \hline \hline
**Problem** & **Number of Variables** & **Number of LIA Constraints** & **Number of Clauses** \\ \hline _ran1_ & 5 & 10 & 20 \\ _ran2_ & 15 & 20 & 40 \\ _ran3_ & 8 & 10 & 20 \\ _ran4_ & 10 & 20 & 50 \\ _ran5_ & 5 & 20 & 40 \\ _ran6_ & 5 & 15 & 40 \\ _ran7_ & 8 & 20 & 50 \\ _ran8_ & 7 & 20 & 50 \\ _ran9_ & 7 & 20 & 80 \\ _ran10_ & 8 & 20 & 100 \\ _ran11_ & 9 & 20 & 50 \\ _ran12_ & 8 & 16 & 80 \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Properties of test problems with random structure. \begin{table}
\begin{tabular}{c c c c c c c c c c} \hline \hline \multirow{2}{*}{**Problems**} & \multicolumn{2}{c}{**Exact Method**} & \multicolumn{2}{c}{**MCMC-Flat\({}^{1/2}\)**} & \multicolumn{4}{c}{**MCMC-Flat\({}^{1/t-\text{pv}}\)**} \\ \cline{2-10}  & **Vol.** & **Time** & **Vol.** & **Time** & **RE (\%)** & **SR** & **Vol.** & **Time** & **RE (\%)** & **SR** \\ \hline \(s1\) & 4 & 0 & 16.11 & 1.31 & 302.69 & 1.0 & 15.92 & 1.07 & 297.97 & 1.0 \\ \(s2\) & 16 & 0 & 25.38 & 1.56 & 58.61 & 1.0 & 36.19 & 1.07 & 126.21 & 1.0 \\ \(s3\) & 64 & 0 & 95.71 & 0.47 & 49.54 & 1.0 & 99.94 & 1.07 & 56.15 & 1.0 \\ \(s4\) & 256 & 0 & 322.06 & 0.14 & 25.80 & 1.0 & 322.71 & 1.06 & 26.06 & 1.0 \\ \(s5\) & 1024 & 0 & 1215.48 & 0.19 & 18.70 & 1.0 & 1137.09 & 1.05 & 11.04 & 1.0 \\ \(s6\) & 4096 & 0 & 4478.05 & 0.17 & 9.33 & 1.0 & 4327.27 & 1.04 & 5.65 & 1.0 \\ \(s7\) & 16129 & 0 & 17,020.84 & 0.06 & 5.53 & 1.0 & 16,396.42 & 0.98 & 1.66 & 1.0 \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Comparison of Exact Method and MCMC-Flat methods on structural problems. the running time of MCMC-Flat\({}^{1/2}\). For example, MCMC-Flat\({}^{1/2}\) takes more than 2000 s on instances _ran2_, _ran5_, and _ran9_, whereas MCMC-Flat\({}^{1/\text{t-pv}}\) takes at most 205.18 s for _ran9_. Note that the relative errors of MCMC-Flat\({}^{1/2}\) and MCMC-Flat\({}^{1/\text{t-pv}}\) on _ran2_, _ran5_, and _ran9_ are close.