Impact of Community Structure on SAT Solver Performance (Презентации лекций), страница 3

Small LBD learnt clauses addstronger constraints between fewer communities. This may allow the solver tofocus its search on a smaller part of the search tree, avoiding scattering, thephenomena where the solver jumps between lots of communities creating learntclauses that link these communities together thus making the structure of theSAT instance worse and consequently harder to solve. We think this study givesa new point of view of LBD and provides a new explanation of its efficiency. Ofcourse, there exists a few cases that do not exhibit such a relationship. This isthe case, for example, for the last example provided in the Figure 1.c. In thisinstance, it seems that in many cases all learnt clauses involve 15 communitiesand more than ten decision levels.We do not yet have strong evidence that correlates classes of instance, and theaverage number of communities that a learnt clause belongs to.

Our suspicion isthat all the original problems for which CDCL solvers were designed, the BMCproblems, may exhibit a particularly good relationship.3.3How close are Communities and LBD?(a) Cumulative distribution function of stan- (b) Evolution of the standard deviation durdard deviation between different measures ing the searchFig. 2: Some standard deviations. This figure is analysed Section 3.3If the LBD seems heavily related to communities, the question is now howclose to the LBD is it? In particular, on some extreme cases, the simple size ofa clause could be a good predictor for its number of communities (clearly, thelarger the clause is, the bigger the number of communities can be).

Thus, wealso have to ensure that (1) the LBD score is more accurate than the size of theclause for predicting the number of communities and (2) the more we update theLBD, the closest we are to the number of communities (the solver is consistentalong its search).In answer to the above question we present two figures: 2.a and 2.b. For bothfigures we computed each problem instance X, for each learnt clause c duringthe first 100,000 conflicts of Glucose solving X, the standard deviation δX of thevalues:1. |LBD(c) − #Com(c)|, representing the dispersion of the differences betweenthe LBD of a clause c and its number of communities, shown as “LBD andcommunities” in the figure;2.

|size(c) − #Com(c)|, representing the dispersion of the differences betweenthe size of a clause c and its number of communities, shown as “Size andcommunities”;3. |LBD(c) − size(c)|, representing the dispersion of the differences betweenthe LBD of a clause c and its size, shown as “Size and LBD”;In the first experiment, we try to see how close LBD and size are to thenumber of communities. We represent in Figure 2 the cumulative distributionfunction of all the δX for each of the three cases. This figure clearly highlights thatthe relationship between LBD and number of communities is much more accurate(it is less than 0.1 for a large majority of instances) than the relationship betweensize and LBD or between size and communities. Thus, as a first conclusion, we seethat, in the large majority of the cases, the LBD is really close to the number ofcommunities.

The only hypothesis here is that the standard deviation has somemeaning over the analysed data, which seems to be a plausible hypothesis.The last experiment we conducted studies the evolution of LBD scores during the execution of Glucose. We focus now on the values of δX accounting forthe dispersion of values |LBD(c) − #Com(c)| for each instance X.

We comparethe values obtained after 10,000 conflicts with the values obtained after 100,000(shown as “10,000 conflicts” on the figure) and the values obtained after 50,000conflicts with, again, the values obtained after 100,000 (shown as “50,000 conflicts”). The comparison is done by the two scatter plots in Figure 2.b. Twoconclusions can be drawn from this. It seems clear that the longer the solveris running, the more accurate it is at estimating the number of communities ofclauses by the LBD. This may also be explained by the fact that, the longerthe solver is running, the longer it is working on fewer communities/LBD, thusfocusing on small subparts of the problem.

However, which one of these twohypothesis is more accurate is still an ongoing work.3.4Experimental Setup: Correlation between Solve Time andCommunity StructureIn this section, we present the hypothesis that it is possible to correlate thecharacteristics of SAT instance C and the running time of CDCL SAT solversin solving C. Previous attempts in this direction have largely focused on characterising the hardness of solving SAT instances in terms of number of variables,clauses or the clause-variable ratio [9]. In our experiments, we go beyond variables, clauses, and their ratio to also considering number of communities andthe Q value (modularity). To test this hypothesis we performed two experiments.The first experiment we did was to correlate the above-mentioned characteristics and the running time of the MiniSAT solver over all instances in the SAT2013 competition [1].

The second experiment we performed was a controlled one,wherein, we randomly-generated instances varying a subset of their characteristics such as number of variables, clauses, Q value, and number of communitiesand keeping the rest constant. We then ran MiniSAT on these randomly generated instances and recorded its running time.

We then plotted the running timeagainst changing Q to see how the two are correlated. All the data for theseexperiments is available at [13].3.5Community Structure and SAT 2013 Competition InstancesWe performed the following steps in this experiment. First, we attempted tocalculate the community structure of every SAT instance from all categories(hard combinatorial, random, and application) the SAT 2013 competition [1].For this we used the OL algorithm [17].

Due to the size of some of the formula itwas not possible to get this information for every instance. As such we were onlyable to run the community structure analysis on approximately 800 instances.The generated results were then aggregated with the solve time of the MiniSATsolver (from the SAT 2013 competition website [1]) for each instance.The analysis was performed on the log(time) rather than raw recorded timedue to the presence of a large number of timeouts, which would have a skeweddistribution. Having said that, our results are similarly strong without this constraint.

In addition to this, we standardised our data to have a mean of zero anda standard deviation of one. This is standard practice when performing regression on factors that have large differences in scale, and ensures that importanceis not falsely reported based only on scale.After formatting the data as described, we fitted a linear regression modelto it using a stepwise regression technique to choose the best model, this wasidentified as:log(time) = |V | ⊕ |CL| ⊕ Q ⊕ |CO| ⊕ QCOR ⊕ VCLRWhere V is the set of all variables in a formula, CL is the set of all clauses, COQ, and VCLR is the ratiois the set of all communities, QCOR is the ratio of |CO||V |of |CL|.

In this model the ⊕ operator denotes that the factor and all interactionswith all other factors were to be considered. Performing the regression resulted ina residual vs fitted plot, shown in Figure 3(b) where the x-axis shows the fittedvalues and the y-axis shows the residuals. As well as a normal quantile plotshown in Figure 3(a) where the x-axis shows the standardised residuals plottedagainst a randomly generated normally distributed sample with the same meanand standard deviation on the y-axis. In the normal quantile plot, the presenceof a slight curve in the line is indicative that the distribution of the data may bebimodal, as such we are unable to measure confidence intervals for the accuracyof the model. In addition to this, the residual plot shows that the data may bebiased, but at least has relatively even variance.

Unfortunately, the presence ofthe timeout results has played a role in the biased nature of the experiment,however dropping them from the results entirely leads to a bias in the oppositedirection.The adjusted R2 of our model is 0.5159. While this relatively low R2 valueindicates that there is some factor we have not considered, our model is far betterthan any previous model, which relied only on number of variables and clauses.This model, which takes the form oflog(time) = |V | ⊕ |CL| ⊕ VCLRis also given for comparison and results in an adjusted R2 of 0.3148 — makingit significantly less predictive than our model. In addition to this, the moredistinct S shape, and presence of sharp curves in Figure 4(a) shows that thedistribution of the data is less normal.