# 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}{c 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/\text{t-pv}}\)**} \\ \cline{2-11}  & **Vol.** & **Time** & **Vol.** & **Time** & **RE (\%)** & **SR** & **Vol.** & **Time** & **RE (\%)** & **SR** \\ \hline _ran1_ & \(5.86\times 10^{11}\) & \(0.15\) & \(5.84\times 10^{11}\) & \(7.59\) & \(-0.35\) & \(1.0\) & \(5.84\times 10^{11}\) & \(12.65\) & \(-0.51\) & \(1.0\) \\ _ran2_ & MO & \(\backslash\) & \(4.18\times 10^{35}\) & \(2186.25\) & \(\backslash\) & \(1.0\) & \(4.22\times 10^{35}\) & \(62.82\) & \(\backslash\) & \(1.0\) \\ _ran3_ & \(2.71\times 10^{18}\) & \(8.36\) & \(2.72\times 10^{18}\) & \(4.58\) & \(0.04\) & \(1.0\) & \(2.73\times 10^{18}\) & \(14.23\) & \(0.44\) & \(1.0\) \\ _ran4_ & MO & \(\backslash\) & \(5.22\times 10^{23}\) & \(65.51\) & \(\backslash\) & \(1.0\) & \(5.21\times 10^{23}\) & \(74.92\) & \(\backslash\) & \(1.0\) \\ _ran5_ & \(4.02\times 10^{10}\) & \(37.51\) & \(4.06\times 10^{10}\) & \(2087.45\) & \(0.91\) & \(1.0\) & \(4.07\times 10^{10}\) & \(47.05\) & \(1.04\) & \(1.0\) \\ _ran6_ & \(3.84\times 10^{10}\) & \(0.73\) & \(3.81\times 10^{10}\) & \(31.37\) & \(-0.74\) & \(1.0\) & \(3.82\times 10^{10}\) & \(45.65\) & \(-0.59\) & \(1.0\) \\ _ran7_ & MO & \(\backslash\) & \(4.89\times 10^{16}\) & \(474.35\) & \(\backslash\) & \(1.0\) & \(4.85\times 10^{16}\) & \(76.38\) & \(\backslash\) & \(1.0\) \\ _ran8_ & \(1.24\times 10^{14}\) & \(4.36\) & \(1.29\times 10^{14}\) & \(188.96\) & \(4.25\) & \(1.0\) & \(1.27\times 10^{14}\) & \(73.15\) & \(2.07\) & \(1.0\) \\ _ran9_ & \(3.14\times 10^{16}\) & \(3625.2\) & \(3.13\times 10^{16}\) & \(3266.07\) & \(-0.33\) & \(0.1\) & \(3.15\times 10^{16}\) & \(205.18\) & \(0.22\) & \(1.0\) \\ _ran10_ & MO & \(\backslash\) & \(3.20\times 10^{17}\) & \(476.1\) & \(\backslash\) & \(0.5\) & \(3.25\times 10^{17}\) & \(378.83\) & \(\backslash\) & \(1.0\) \\ _ran11_ & MO & \(\backslash\) & \(2.90\times 10^{19}\) & \(655.12\) & \(\backslash\) & \(1.0\) & \(2.94\times 10^{19}\) & \(76.85\) & \(\backslash\) & \(1.0\) \\ _ran12_ & \(5.23\times 10^{18}\) & \(709.74\) & \(5.21\times 10^{18}\) & \(45.94\) & \(-0.35\) & \(1.0\) & \(5.21\times 10^{18}\) & \(196.62\) & \(-0.27\) & \(1.0\) \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Comparison of Exact Method and MCMC-Flat methods on random instances. and the number of valuations in the space, respectively. The \"Volume/Space\" column is the proportion of the number of models to the size of the space, where \"NA\" represents an unknown property. Intuitively, a problem with lower Volume/Space is more constrained. We take an exact model counter Volce+LattE [9] and two approximate model counters SMTApproxMC [19] and ApproxMC2 [21] for comparison. Note that all the three are state-of-the-art model counters. To run them, the benchmark problems were converted to their corresponding formats. The problem format in [24] is similar to that of our methods' accepts. However, the format is quite different from the formats of Volce+LattE, SMTApproxMC, and ApproxMC2. Volce+LattE accepts an input format called the \"Enhanced DIMACS CNF Format\", whereas SMTApproxMC accepts SMT-LIB2 format of Bit Vector theory. In our implementation, we first translate the instances from [24] into the \"Enhanced DIMACS CNF Format\" of Volce+LattE. Specifically, denominators of coefficients in a LIA constraint are all multiplied by their least common multiple. For example, the translation result of (7) is,

\[-20\cdot x_{1}-16\cdot x_{2}-56\cdot x_{3}+28\cdot x_{4}+15\cdot x_{5}\leq-24. \tag{8}\]

In this way, every coefficient in an LIA constraint is a number, instead of a fraction. In addition, every value bound for a variable is translated into a corresponding inequality. Moreover, due to that each problem instance representing a convex body, our converter states that all constraints must be satisfied.