The Impact of Entropy and Solution Density on Selected SAT Heuristics

Abstract

We present a new characterization of propositional formulas called entropy, which approximates the freedom we have in assigning the variables. Like several other such measures (e.g., back-door and back-door-key variables), it is computationally expensive to compute. Nevertheless, for small and medium-size satisfiable formulas, it enables us to study the effect of this freedom on the impact of various SAT heuristics, following up on a recent study by C. Oh (Oh, SAT’15, LNCS 9340, 307–323). Oh’s findings were that the expected success of various heuristics depends on whether the input formula is satisfiable or not. With entropy, and also with the measure of solution density, we are able to refine these findings for the case of satisfiable formulas. Specifically, we found empirically that satisfiable formulas with small entropy “behave” similarly to unsatisfiable formulas.

1. Introduction

In [1], Oh examined the impact of various key heuristics in competitive SAT solvers (i.e., solvers of the propositional satisfiability problem). His key findings were that the average success of those heuristics depends on whether the input formula is satisfiable or not. In particular the effect of the deletion strategy, restart policy, decay factor, and database reduction is different, on average, between satisfiable and unsatisfiable formulas. This observation can be used for designing solvers that specialize in one of them, and for designing a hybrid solver that alternates between SAT/UNSAT “modes”. Indeed certain variants of COMiniSatPS [1] work this way.

We do not see an a priori reason to believe that the SAT/UNSAT divide—corresponding to the distinction between zero or more solutions—explains best the differences in the effect of the various heuristics (we note that while proving Unsat and Sat belong to separate complexity classes, there is no known connection of this fact to effectiveness of heuristics). In this work we investigate further his findings, and show empirically that there are more refined measures (i.e., properties of the input formula) than the satisfiability of the formula, that predict better the effectiveness of these heuristics. In particular, we checked how it correlates with two measures of satisfiable formulas: the entropy of the formula (to be defined below), which approximates the freedom we have in assigning the variables, and the solution density (henceforth density), which is the number of solutions divided by the search space. Our experiments show that both are correlated with the effectiveness of the heuristics, but the entropy measure seems to be more consistent: in all experiments, with both random and industrial-like benchmarks, heuristics that are better for unsat formulas are also better for formulas with low entropy. The results for density are less consistent.

Like several other measures that were proposed in the past (e.g., back-door variables and back-door key variables [2]), both measures are hard to compute. They require solving a #p problem over a SAT formula, and hence at least for now we cannot see a direct application of these results for faster SAT solving of industrial formulas. This does not mean that these results are useless in the long run, however. In particular our contributions are:

• Suggesting the concept of entropy as a new proxy to the freedom of variables,
• Showing evidence that for satisfiable formulas there are better predictors of the effectiveness of various SAT heuristics than the sat/unsat dichotomy suggested by Oh, and in particular that entropy predicts hardness consistently across all those heuristics (albeit not in all cases with strong statistical significance), and
• Setting the foundations for future research into approximating entropy fast, which may eventually indeed lead to constructing faster portfolios based on entropy-based hardness prediction.

We continue in the next section by describing the concept of entropy and its relevance to SAT formulas. In Section 3 we explain the statistical methods that we used in this research. Section 4 is the main section of this article. It describes in detail our experimental setting and our empirical findings. Our conclusions from this research appear in Section 5.

2. Entropy

Let $\phi$ be a propositional CNF formula, $var\left(\phi \right)$ its set of variables and $lit\left(\phi \right)$ its set of literals. In the following we will use $v,\overline{v}$ to denote the literals corresponding to a variable v when the distinction between variables and literals is clear from the context. If $\phi$ is satisfiable, we denote by $r\left(l\right)$, for $l\in lit\left(\phi \right)$, the ratio of solutions to $\phi$ that satisfy l. Hence for all $v\in var\left(\phi \right)$, it holds that $r\left(v\right)+r\left(\overline{v}\right)=1$. We now define:

Definition 1

(variable entropy). For a satisfiable formula $\phi$, the entropy of a variable $v\in var\left(\phi \right)$ is defined by

$$e\left(v\right)\doteq -r\left(v\right){log}_{2}r\left(v\right)-r\left(\overline{v}\right){log}_{2}r\left(\overline{v}\right).$$

(1)

where $0·{log}_{2}0$ is taken as being equal to 0.

This definition is inspired by Shannon’s definition of entropy in the context of information theory [3]. Figure 1 (left) depicts (1).

Intuitively, entropy reflects how “balanced” a variable is with respect to the solution space of the formula. In particular $e\left(v\right)=0$ when $r\left(v\right)=0$ or $r\left(v\right)=1$, which means that $\phi \Rightarrow \overline{v}$ or $\phi \Rightarrow v$, respectively. In other words, $e\left(v\right)=0$ implies that v is a backbone variable, since its value is implied by the formula. The other extreme is $e\left(v\right)=1$; this happens when $r\left(v\right)=r\left(\overline{v}\right)=0.5$, which means that v and $\overline{v}$ appear an equal number of times in the solution space.

Definition 2 (formula entropy).

The entropy of a satisfiable formula is the average entropy of its variables.

As an example, Figure 1 (right) is a histogram of $e\left(v\right)$ for a particular formula $\phi$, where for 24 out of the 100 variables $r\left(v\right)=0$.

Entropy is hard to compute: Let $\#SAT\left(\phi \right)$ denote the number of solutions a formula $\phi$ has. Then it is easy to see that

$$r\left(v\right)=\frac{\#(\phi \wedge v)}{\#\phi }\mathrm{and}r\left(\overline{v}\right)=1-r\left(v\right).$$

(2)

Hence computing $e\left(v\right)$ amounts to two calls to a model counter. However, since the denominator $\#\phi$ is fixed for $\phi$, computing $e\left(\phi \right)$ amounts to $\left|var\right(\phi \left)\right|+1$ calls to a model counter. Since model counting is a #P problem, we can only compute this value for relatively small formulas.

3. A Preliminary: Standardized Linear Regression

We assume the reader is somewhat familiar with linear regression. It is a standard technique for building a linear model $\widehat{y}={\widehat{\beta }}_0+{\widehat{\beta }}_{1}x$, where $\widehat{y}$ in our case is a predictor of the number of conflicts, and x is either the entropy or the density of the formula. We will focus on two results of linear regression: the value of ${\widehat{\beta }}_1$ and the p-value. The latter is computed with respect to a null hypothesis, denoted $H_0$, that ${\widehat{\beta }}_1=0$, and an alternative hypothesis $H_1$. $H_1$ can be either the complement of $H_0$ (${\widehat{\beta }}_1\ne 0$) or a “one-sided hypothesis”, e.g., $H_1:{\widehat{\beta }}_1>0$. In the former case, $p=2Pr(Z\le z\mid H_0)$, where $Z\sim N(0,1)$ and $z=\frac{{\widehat{\beta }}_1-0}{\mathrm{std}\left({\widehat{\beta }}_1\right)}$. The ‘0’ in the numerator comes from the specific value in $H_0$. In other words, assuming $H_0$ is correct, the p-value indicates the probability that a random value from a standard normal distribution $N(0,1)$, is less than z, the standardized value of ${\widehat{\beta }}_1$. In the latter case $p=Pr(Z\le z\mid H_0)$.

We list below several important points about the analysis that we applied.

• Standardization of the data: given data points $X\doteq x_1,\dots ,x_n$, their standardization $X^{\prime }\doteq x_1^{\prime },\dots ,x_n^{\prime }$ is defined for $1\le i\le n$ by

  $$x_i^{\prime }=\frac{x_i-\overline{x}}{\sigma },$$

  where $\overline{x}$ is the average value of X and $\sigma$ is its standard deviation. Now $X^{\prime }$ has no units, and hence two standardized sets of data are comparable even if they originated from different types of measures (in our case, entropy and density). All the data in our experiments was standardized.
• Bootstrapping: Bootstrapping, parameterized by a value k, is a well-known technique for improving the precision of various statistics, such as the confidence interval. Technically, bootstrap is applied as follows: Given the original n samples, uniformly sample it n times with replacement (i.e., without taking the sampled points out, which implies that the same point can be selected more than once); repeat this process k times. Hence we now have $n·k$ data points. For our experiments we took $k=1000$, which is a rather standard value when using this technique. In each of the experiments that will be reported later on $n=5000$, hence we have a total of $5\times {10}^6$ data points for each experiment.
• Two regression tests: The entropy and density data consists of pairs of the form $\langle entropy,conflicts\left[i\right]\rangle$, and $\langle density,conflicts\left[i\right]\rangle$, respectively, where $i\in \{1,2\}$ is the index of the heuristic (e.g., in Section 4.3 we will compare the effectiveness of two restart strategies, so the indices 1 and 2 refer to those strategies). Hence the corresponding data is four series of points $(e_1,c_1\left[i\right]),\dots ,(e_n,c_n\left[i\right])$, and $(d_1,c_1\left[i\right]),\dots ,(d_n,c_n\left[i\right])$, where $i\in \{1,2\}$. To compare the predictive power of entropy, density and Oh’s criterion of SAT/UNSAT, we performed two statistical tests (recall that the data is standardized, and hence comparable):

  –

  The $\Delta$ test: A linear regression test over the series $(e_1,c_1\left[1\right]-c_1\left[2\right])\dots$ $(e_n,c_n\left[1\right]-c_n\left[2\right])$, and the series $(d_1,c_1\left[1\right]-c_1\left[2\right])\dots (d_n,c_n\left[1\right]-c_n\left[2\right])$.

  –

  The ${\Delta }_{{\widehat{\beta }}_1}$ test: A linear regression test over the series $(e_1,c_1\left[1\right])\dots (e_n,c_n\left[1\right])$ and $(e_1,c_1\left[2\right])\dots (e_n,c_n\left[2\right])$, and similarly for density (i.e., four tests all together). We then checked the significance of ${\widehat{\beta }}_1$ for each of these 4 tests. In addition, we checked the hypothesis $H_0:{\widehat{\beta }}_1\left[1\right]-{\widehat{\beta }}_1\left[2\right]=0$ for each of the measures. The result of this last test appears in the Appendix A.

  Intuitively, the two models tell us slightly different things: the first tells us whether the gap between the two heuristics is correlated with the measure, and the second tells us whether there is a significant difference in the value of ${\widehat{\beta }}_1$ (the slope of the linear model) between the two heuristics. As we will see in the results, the p-value obtained by these models can be very different.
• Plots: The plots are based on the original (non-standardized) data. To reduce the clutter (from 5000 points), we rounded all values to 2 decimal points and then aggregated them. Aggregation means that points $(x,y_1)\dots (x,y_n)$ (i.e., n points with an equal x value) are replaced with a single point ($x,$ $avg(y_1\dots y_n)$). However the trend-lines in the various plots are depicted according to the original data, before rounding and aggregation. The statistical significance of these trend-lines appears in the Appendix A.

4. Empirical Findings

4.1. The Benchmark Set

All the results that we report below are based on experiments with 10,000 CNF formulas, divided to two equally sized subsets described below. For each such formula, we calculated the exact entropy and solution density, using a combination of the SAT-based model-counters Cachet [4] and SharpSAT [5]. To the best of our knowledge currently these are the most powerful exact model-counters. We note that in addition to SAT-based model-counters, there is also an option of building an Ordered Binary Decision Diagram (OBDD) from the input formula, and then the counting is polynomial in the size of the BDD. The problem is that the BDD itself can become exponential in the number of variables. Some recent examples of applying BDD-based counting include [6,7,8].

The first subset of benchmarks is comprised of 5000 3-SAT random formulas with 100 variables and 400 clauses. These are formulas taken from SAT-lib, in which the number of backbone variables is known. Specifically, there is an equal number of formulas in this set with 10, 30, 50, 70 and 90 backbone variables (i.e., a 1000 formulas of each number of backbone variables), which gave us a near-uniform distribution of entropy among the formulas.

The second subset of benchmarks is comprised of 3296 CNF formulas that are generated with the modularity-based CNF generator modularityGen [9], which generates random formulas that have characteristics of real-world problems (out of the 5000 formulas that we generated, this is the number of formulas for which we were able to compute entropy and solution density within the timeout that we set). To understand the structure of these formulas, note first that a CNF formula can be represented by the variable incidence graph, which is an undirected graph in which variables are nodes and two nodes are connected if they share a clause. Such a graph can be partitioned into sets of nodes, and each partition is called a community. Given a partition we can measure the ratio between the number of edges within communities (in contrast to edges between communities) and the number of such edges that we would have gotten had we distributed the same number of edges between the same nodes but in a uniformly random fashion. Between all possible partitions, we take the one that drives this ratio to maximum: this is called the modularity of the graph, and is typically denoted by Q [10]. It has been recognised in [11] and later in [12] that industrial CNF formulas have high values of Q (a “good community structure”), and moreover that heuristics used by modern SAT solvers (unknowingly) exploit this fact for faster solving. In an impressive series of experiments reported in [9], they generated hundreds of formulas with a varying value of Q. They then took two solvers, March [13] and Glucose [14], which specialize in random and industrial formulas, respectively, and ran them with those benchmarks as input. Exactly as expected, March was far better with formulas having low values of Q and Glucose was much better with formulas having high values of Q.

modularityGen gives the user the ability to control, among other things, the modularity Q, the number of neighborhoods n, and the size of the formula. For our experiments we chose $Q=0.7$ (based on measurements made in [9], that showed that most industrial formulas have at least this value of modularity, whereas random formulas have values smaller than $Q=0.3$), $n=5$, 400 variables and 1600 clauses.

To distinguish between the random and modularity-based benchmarks sets, we will call them respectively B-Rand and B-Mod from hereon.

4.2. Entropy and Density Predict Hardness

We checked the correlation between hardness, as measured by the number of conflicts, and the two measures described above, namely entropy and density. We use the number of conflicts as a proxy of the run-time, because these are all easy formulas for SAT, and hence the differences in run-time are rather meaningless. The two plots in Figure 2 depict this data based on our experiments with the solver MiniSat-HACK-999ED. It is apparent that higher entropy and higher density imply a smaller number of conflicts. It turns out that this is not a characteristic that is unique to this solver. We performed a detailed statistical analysis of seven different solvers, and witnessed a similar phenomenon, as we now describe.

Denote by ${{\widehat{\beta }}_1}^E$ and ${{\widehat{\beta }}_1}^S$ the ${\widehat{\beta }}_1$-value of the linear models for entropy vs. conflicts and density vs. conflicts, respectively.

Table 1. For each solver, we list the 95% confidence interval of its ${\widehat{\beta }}_1^E$ (entropy) and ${\widehat{\beta }}_1^S$ (solutions). For all engines the corresponding p-value is practically 0 (i.e., ≤${10}^{-100}$). The last two columns refer to the gap between these measures.

Solver	${\widehat{\mathit{\beta }}}_1^{\mathit{E}}$	${\widehat{\mathit{\beta }}}_1^{\mathit{S}}$	${\widehat{\mathit{\beta }}}_1^{\mathit{E}}-{\widehat{\mathit{\beta }}}_1^{\mathit{S}}$	p-Value
MiniSat-HACK-999ED	(−84.29, −72.58)	(−84.93, −73.56)	(5.37, 16.96)	0.716
MiniSat-HACK-999ED	(−86.31, −75.36)	(−82.97, −72.64)	(−7.51, 1.44)	0.200
(modified to luby)
MiniSat-HACK-999ED	(−72.84, −63.61)	(−72.31, −62.91)	(−4.80, 3.57)	0.738
(modified for 2 phases)
SWDiA5BY	(−91.61, −79.17)	(−90.97, −78.77)	(−5.95, 4.92)	0.84
COMiniSatPS	(−74.68, −64.58)	(−75.41, −65.43)	(−3.79, 5.37)	0.76
lingeling-ayv	(−76.19, −66.61)	(−71.70, −61.76)	(−8.99, −0.35)	0.029
Glucose	(−91.24, −79.34)	(−90.56, −78.88)	(−6.00, 4.85)	0.845

shows strong correlation between both measures to the number of conflicts (the p-value in both cases, for all engines, is practically 0). The last two columns show the gap ${{\widehat{\beta }}_1}^E-{{\widehat{\beta }}_1}^S$ and the corresponding p-value for $H_0:{{\widehat{\beta }}_1}^E-{{\widehat{\beta }}_1}^S=0,H_1:{{\widehat{\beta }}_1}^E-{{\widehat{\beta }}_1}^S\ne 0$, when measured across the $k=1000$ iterations of the bootstrap method that was described in Section 3. For engines with high p-value we cannot reject $H_0$ with confidence.

4.3. A Refinement of Oh’s Results

In this section we describe each of the experiments of Oh [1], and our own version of the experiment based on entropy and density, when applied to the 10,000 benchmarks mentioned above. We omit the details of one experiment, in which Oh examined the effect of canceling database reduction, the reason being that this heuristic is only activated after 2000 conflicts, and most of our benchmarks are solved before that point (we note that our attempt to use an approximate model-counter with larger formulas failed: the inaccuracies were large enough to make the analysis show results that are senseless). Raw data as well as charts and regression analysis of our full set of experiments can be found online in [15].

1. Deletion strategy: Different solvers use different criteria for selecting the learned clauses for deletion. It was shown in [1] that for SAT instances learned clauses with low Literal Block Distance (LBD) [14] value can help, whereas others have no apparent effect. In one of the experiments, whose results are copied here at the top part of Figure 3, Oh compared the criterion of “core LBD-cut” 5 and clause size 12 (an LBD-cut is the lowest value of LBD a learned clause had so far, assuming this value is recalculated periodically). In other words, either save (i.e., do not delete) clauses with an LBD-cut of 5 and lower, or clauses with size 12 or lower. It shows that for UNSAT instances the former is better, whereas the opposite conclusion is reached for the SAT instances. The results of our own experiments are depicted at the bottom of the figure. They show that the latter is indeed slightly better with our benchmarks (all satisfiable, recall). However, what is more important, is that the difference becomes smaller with lower entropy—hence the decline of the trend-lines and the negative ${\beta }_1$ values (recall that the trend-lines are based on the raw data, whereas the diagram itself is computed after rounding and aggregation to improve visibility. Hence occasionally the two do not seem to be perfectly matching). Hence it is evident that formulas with small entropy “behave” more similar to unsat formulas. More information appears in the caption of Figure 3, and in the Appendix A.

2. Deletion with different LBD-cut value Related to the previous heuristic, in [1] it was found that deletion based on larger LBD-cut values, up to a point, improve the performance of the solver with unsat formulas, but not with SAT ones. Figure 4 (top) is an excerpt from his results for various LBD-cut values. We repeated his experiment with LBD-cut 1 and LBD-cut 5. The plots show that lower values of entropy yield a bigger advantage to LBD-cut 5, which again demonstrates that satisfiable formulas with these values ‘behave’ similarly to unsat formulas. The results for density are inconsistent, in the sense that we see the same phenomenon with B-Rand but not with B-Mod.

3. Restarts policy: The Luby restart strategy [16] is based on a fixed sequence of time intervals, whereas the Glucose restarts are more rapid and dynamic. It initiates a restart when the solver identifies that learned clauses have higher LBD than average. According to the competitions’ results this is generally better in unsat instances. Oh confirmed the hypothesis that this is related to the restart strategy: indeed his results show that for satisfiable instances Luby restart is better.

Our own results can be seen in Figure 5. The fact that the gap in the number of conflicts between Luby and Glucose-style restarts is negative, implies that the former is generally better, which is consistent with Oh’s results for satisfiable formulas. Observe that the trend-line declines with entropy (${\widehat{\beta }}_1=-15$ and ${\widehat{\beta }}_1=-164$ for the two benchmark sets), which implies that Glucose restarts are statistically better with low entropy. So again we observe that low entropy formulas ‘behave’ more similar to UNSAT formulas than those that have high entropy. We speculate that with high-entropy instances, the solver hits more branches that can be extended to a solution, hence Glucose’s rapid restarts can be detrimental. Density again seems to have an inconsistent effect between the two benchmark sets.

4. The variable decay factor: This experiment shows the most consistent and the most statistically significant results. The well-known VSIDS branching heuristic is based on an activity score of literals, which decay over time, hence giving higher priority to literals that appear in recently learned clauses. In the solver MiniSat_HACK_999ED, there is a different decay factor for each of the two restart phases: this solver alternates between a Glucose-style (G) restart policy phase and a no-restart (NR) phase (these two phases correspond to good heuristics for SAT and UNSAT formulas, respectively). In [1] Oh compares different decay factors for each of these restart phases on top of MiniSat_HACK_999ED. His results show that for UNSAT instances slower decay gives better performance, while for SAT instances it is unclear. His results appear at the top of Figure 6. We experimented with the two extreme decay factors in that table: 0.95 and 0.6. Please note that since our benchmarks are relatively easy, the solver never reaches the NR phase. The plot shows the gap in the number of conflicts between these two values. A higher value means that with strong decay (0.6) the results are worse. We can see that the results are worse with strong decay when the entropy is low, which demonstrates again that the effect of the variable decay factor is similar for unsat formulas and satisfiable formulas with low entropy. A similar phenomenon happens with small density in both benchmark sets.

5. Conclusions

We defined the entropy property of satisfiable formulas, and used it, together with solution density, to further refine and investigate the results achieved by Oh in [1]. We began by showing a clear correlation between these two measures and the number of conflicts in Section 4.2, based on an analysis of seven different solvers. We then showed that both measures predict better the effect of various SAT heuristics than Oh’s sat/unsat divide, and that satisfiable formulas with small entropy ‘behave’ similarly to unsatisfiable formulas. In that respect the entropy measure is more consistent than density across benchmarks types. Since both measures are hard to compute we do not expect these results to be applied directly (e.g., in a portfolio), but perhaps future research will find ways to cheaply approximate them and lead to improved heuristics.