# 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  
In this subsection, we propose a MCMC method to solve the #SMT(LIA) problem based on the flat histogram method. In the proposed method, we make each random move follow the probability specified in Equation (1). Therefore, our method avoids using Metropolis sampling, and visits states at every energy level equally often. However, the density function \(n(\cdot)\) in Equation (1) is not known a priori. To handle this, we use a changing current estimate \(n^{\prime}(\cdot)\) to approximate \(n(\cdot)\). Initially, \(n^{\prime}(E)\) is set to 1 for every energy level \(E\). With the initial values of \(n^{\prime}(\cdot)\), our algorithm samples the space with increasing the visit histogram \(H(\text{g}(\sigma))\) by 1 and update \(n^{\prime}(\text{g}(\sigma))\) with a _modification factor_\(F\), every time a valuation \(\sigma\) is visited. Specifically, the estimate of DOS is updated by  
\[n^{\prime}(g(\sigma))\gets n^{\prime}(g(\sigma))\times F. \tag{5}\]  
The sampling process repeats until the visit histogram \(H(\cdot)\) is sufficiently flat. If \(F\) does not reach its designated value, a new sampling process is started with resetting \(H(\cdot)\) and starts with a refinement of \(F\). The role of \(F\) will be explained next. An outline of the _MCMC-Flat algorithm_ is shown in Algorithm 1. It returns the estimate \(n^{\prime}(0)\). As is seen at the end of Algorithm 1, the information in \(n^{\prime}(\cdot)\) reflects the relative density of each energy level. To obtain the real density of each level, we normalize \(n^{\prime}(\cdot)\) w.r.t. the volume of the sampling area. For a SMT(LIA) formula \(\phi\) defined on \(K\) numeric variables and each has the same range \([lb,ub]\) (\(lb\) is the lower bound and \(ub\) is the upper bound), the volume of the sampling area is \((ub-lb)^{K}\). Therefore, the volume of \(\phi\) is obtained by  
\[\frac{n^{\prime}(0)}{\sum\limits_{e\in E}n^{\prime}(e)}\times(ub-lb)^{K}. \tag{6}\]```
\(N^{\prime}(E)\gets 1\) for every energy level \(E\) \(F\gets F_{0}\)  Randomly generate a valuation \(\sigma\) \(n^{\prime}(\sigma)\gets n^{\prime}(\sigma)\times F\) \(H(\sigma)\gets H(\sigma)+1\) repeat  repeat  Generate a new valuation \(\sigma^{\prime}\) if\(n^{\prime}(g(\sigma^{\prime}))<n^{\prime}(g(\sigma))\)then \(\sigma\gets\sigma^{\prime}\) else  Move to \(\sigma^{\prime}\) with probability defined in Equation (2) endif \(n^{\prime}(\sigma)\gets n^{\prime}(\sigma)\times F/\)/reweighting the density \(H(\sigma)\gets H(\sigma)+1/\)/increase the visit histogram untilIsFlat(H) \(F\leftarrow\textit{Update}(F)\) // prepare to a new sweep \(H(E)\gets 0\) for every \(E\) until\(F\) is close enough to \(F_{final}\)  Normalize \(n^{\prime}\) return\(n^{\prime}(0)\) using Equation (6)
```

**Algorithm 1**_MCMC-Flat for #SMT(LIA)_

### Updating Strategy for the Modification Factor

In Algorithm 1, the modification factor \(F\) is used to reweight the density of states. The outer loop updates \(F\) at each iteration with the function _Update(F)_. Two strategies of updating \(F\) were studied. * MCMC-Flat\({}^{1/2}\) (the \(1/2\)-strategy): Initially, set \(F\) to \(1.5\), and update \(F\) to \(F^{1/2}\) when \(H\) is flat. Each time \(F\) is updated, reset \(H(\cdot)\)[14]. * MCMC-Flat\({}^{1/t}\) (the \(1/t\)-strategy): Initially, set \(F\) to \(1.0\). After a constant MC time (e.g., \(1000\)), check \(H(E)\), and if \(H(E)\
eq 0\) for all \(E\) then refine \(F\gets F/2\) and reset H(\(\cdot\)). If \(F\leq 1/t\) (\(t=j/N\), \(j\) is the number of trails and \(N\) is the number of energy levels.) then F \(\gets 1/t\) and keep the value in following trails. If \(F<F_{final}\), we stop the sampling process [25]. [PERSON] et al. (2015) showed that the \(1/t\) strategy can lead to a smaller error than the \(1/2\) strategy. We also verified this behavior on a small set of test problems. So, we focus on studying the performance of MCMC-Flat\({}^{1/t}\) on the #SMT(LIA) problem.