# 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
One of our important findings is that the flatness condition for \(H(\cdot)\) is difficult to reach for some test problems. Next, we will examine the notion of flatness of a visit histogram and introduce a new rule to evaluate flatness. ### Evaluating the Flatness of Visit Histogram

One method to evaluate the flatness of the visit histogram \(H\) is based on its minimum value \(min\) and maximum value \(max\)[14]. Specifically, \(H\) is considered to be flat if \(max\ -\ min<\delta\ \times\ max\), where \(\delta\) is a pre-set constant parameter. Obviously, the more flat \(H\) is (i.e., with smaller \(\delta\)) the more uniformly Algorithm 1 visits each energy level. However, with smaller \(\delta\) we need more sampling steps. Furthermore, literature [26] pointed out that the flatness is not a good indicator for convergence. Among other works, [PERSON] and [PERSON] [25] introduced a condition to evaluate the visits of each energy level: every energy level must be visited one time. We tested MCMC-Flat\({}^{1/t}\) with this condition on one of our random problems and found that MCMC-Flat\({}^{1/t}\) does not converge. In particular, with this condition the relative error of MCMC-Flat\({}^{1/t}\) stays at \(-1.0\) (see Figure 3a). One of the underlying reasons, as we conjecture, is that the number of states of a particular energy level is very large for SMT(LIA) formulas with many variables (a.k.a. high dimensions). So, MCMC-Flat\({}^{1/t}\) needs many trails to visit every energy level and to fulfil the condition for the visit histogram. To overcome the shortcomings, we introduce a new rule to analyze the visit histogram (as shown in Algorithm 2). Algorithm 2 marks one unvisited energy level as visited and then returns, each time it is called (i.e., do a pseudo sampling), while it does not stop the current sampling process. This behavior will force the sampling process do another sweep on energy levels. Note that a sweep will require more Monte Carlo trials. In the worst case, Algorithm 2 will force the sampling process to make \(N\) sweeps, where \(N\) is the number of energy levels. The amount of sweeps shall be enough to visit each energy level. We call Algorithm 1 with this method MCMC-Flat\({}^{1/t-pv}\). The behaviour of MCMC-Flat\({}^{1/t-pv}\) is shown in Figure 3b. It can be seen that MCMC-Flat\({}^{1/t-pv}\) converges (with a decreasing relative error) when the modification factor \(F\) is decreasing. Note that in our method, \(F\) initially takes 1.0, and is reduced in the following iterations. What we expect is that the smaller \(F\) is, the more accurate our method's estimate of \(n(0)\) is. ```
Input: A visit histogram \(H\) Output: A Boolean value indicates if every energy is visited for each \(i\) in \(H\) if\(H[i]=0\) \(H[i]\gets 1\) return false endif endfor return true
```

**Algorithm 2**Pseudo Visit (PV) of Histogram

## 5 Experimental Evaluation

This section consists of two parts. In the first part, we show the accuracy and efficiency of the proposed algorithms on structured and random SMT(LIA) instances. In the second part, we compare our techniques with VolCE+LatTE [9], SMTApproxMC [19] and ApproxMC2 [21], on hard convex bodies (where every linear integer constraint is joined by conjunction) instances extracted from the benchmark suit of [24]. Figure 3: Dynamical behavior of MCMC-Flat\({}^{1/t}\) and MCMC-Flat\({}^{1/t-pv}\) on the same test problem: (**a**) MCMC-Flat\({}^{1/t}\) does not converge when \(F\) is small enough; (**b**) MCMC-Flat\({}^{1/t-pv}\) converges when \(F\) is small enough. In the first part, every structured instance is defined in a two-dimensional space (i.e., involving two numeric variables) containing a single square of varying volumes. The random instances contain different numbers of variables, LIA constraints, and clauses. The Exact Method presented in [18] is used as a reference. Properties of random instances are shown in Table 1.

All the experiments were run on a Linux system with a CPU running at 2.53 GHz, 60 min time limit and 2 GB memory limit.