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

This result is confirmed when using theKolomogorov-Sminov (KS) method to test goodness of fit. Our model results inResiduals vs Fitted10Residuals-10-4-3-2-2Standardized residuals2243Normal Q-Q243405286243405286-3-2-10123-2Theoretical Quantileslm("ltime~clauses*vars*Q*coms*Q_coms*vars_clauses")-101Fitted valueslm("ltime~clauses*vars*Q*coms*Q_coms*vars_clauses")(a) Plot of normal and theoreticalquantiles(b) Residuals vs Fitted valuesFig.

3: Plots for the model including community metrics R2 = 0.5159Residuals vs Fitted0-1Residuals-20-3-2Standardized residuals212Normal Q-Q-4243-3405286-4243405286-2-10123Theoretical Quantileslm("ltime~vars*clauses*vars_clauses")(a) Plot of normal and theoreticalquantiles-2.0-1.5-1.0-0.50.00.51.0Fitted valueslm("ltime~vars*clauses*vars_clauses")(b) Residuals vs Fitted valuesFig. 4: Plots for the model without community metrics R2 = 0.3148a KS value of 0.1283 compared with the previously available model which gavea KS value of 0.3154, this lack of normality makes it impossible to estimateconfidence intervals for the results. However, it is possible to rank the factors byimportance (because the data was standardised prior to regression). The resultsin Figures 3(a) and 3(b) show that our model, while not perfect, is a major steptowards being a predictor for solve time. This is confirmed when viewing theresults of the regression shown in the Table 1 (This table can also be viewedfrom our website [13]).Bottomline Result: The main result we found from the regression is thatthe Q factor is involved in every one of the significant interactions at a 99.9%confidence level.

In addition to this we found that |V | (number of variables)alone is not significant, and |CL| (number of clauses) alone is only marginallysignificant. Furthermore, |CO| (number of communities) proved to be the mostpredictive effect, as well as being involved with numerous other interactions thatare also significant.3.6Community Structure and Random InstancesIn this Section, we describe the experiments, where we ran MiniSAT on a largeset of randomly-generated SAT instances, to better understand the effects ofvarying the various factors of the input formulas in a controlled fashion. We rana controlled experiment in which approximately 550,000 formulas were generatedand executed. In performing this experiment we discovered that there is a largeincrease in average solution time when the 0.05 ≤ Q ≤ 0.13. This can be seenclearly in Figure 5(a).The formulas were generated by varying the number of variables from 500 to2000 in increments of 100, the number of clauses from 2000 to 10,000 in increments of 1000, the desired number of communities from 20 to 400 in incrementsof 20, and the desired Q value, from zero to one in increments of 0.01.

Eachindividual trial was repeated three times with the same characteristics. This wasnecessary due to the non-deterministic nature of the generation technique. Theresulting experiments were ran in a random order for several hours to generatea large volume of data.To generate a specific instance we perform the following actions: Let usassume that the set of variables be denoted as V = {Vi : 0 ≤ i < nv } wherenv is the desired number of variables. Similarly, let the set of groups beG = {Gx : 0 ≤ x < ng } where ng is the desired number of groups.

A group isa rough estimate of a community, and is used only to guide the generator inproducing a structured problem.First, we assign variables to groups such that each group|Gx = {Vy : y = rv ∗ |G| + x; 0 ≤ rv < |V|G| }, where rv is randomly selected.Next, we generate the set of clauses C = {Cz : 0 ≤ z < nc } as follows, wherenc is the desired number of clauses such that Cz = {Vz1 ∨ Vz2 ∨ Vz3 }.

Eachclause is constructed as follows: First, a group Gx and a variable Vz1 ∈ Gxare randomly selected. This is followed by a selection of another variable Vz2Factor|CO||CL| Q QCOR|CL| Q|CL| Q |CO| QCOR V CLR|CL| Q |CO|Q QCORQEstimate-1.237e+00-4.226e+02-2.137e+02-1.177e+03-6.024e+023.415e+021.726e+02Std. Error t value P r(> |t|)3.202e-01 -3.864 0.0001211.207e+02 -3.500 0.0004926.136e+01 -3.483 0.0005233.461e+02 -3.402 0.0007021.774e+02 -3.396 0.0007191.023e+023.339 0.0008815.200e+013.318 0.000947Sig*********************Table 1: List of the factors with 99.9% significance level. indicates an interaction between two or more factors and Sig stands for Significance. The full tableis listed in Appendix Table 2Q Against Time(Uniform Random Sample)600500400300Time in Seconds20000100200100Time in Seconds700800300900Average Q Against Time00.10.20.30.40.50.60.70.80.9Q(a) Average Time100.200.300.400.500.600.700.80Q(b) Stratified Sample(c) All instancesFig.

5: A plot of Q against time, for three different data setsfrom either Gx or V with probability of q of being selected from Gx . Finally, athird variable Vz3 is selected from either Gx or V with probability of q of beingchosen from Gx . The value q (lies between 0 and 1) can be used as a roughestimator of Q, the modularity of the formula and is provided as input to thegenerator. The result is a randomly-generated 3-CNF formula.During our analyses of the results, we discovered that our random generationtechnique resulted in far more results in the 0.05 ≤ Q ≤ 0.12 range than in anyother range.

To ensure that the results seen were not because of this discrepancy,we re-ran many of the trials, focusing on data outside of this range, and generatedapproximately another 307,000 formula.To ensure an unbiased analyses we also performed basic analyses on a stratified random sample taken uniformly across the range of Q.

From the 545,000results 2250 were randomly sampled, with 250 results taken from each rangeof 0.1, as there were no results with Q > 0.9 this range was not included inthe sample. This process ensured their was no bias in the results based purelyon frequency. The resulting sample is shown in Figure 5(b) which shows thatwhen 0.05 ≤ Q ≤ 0.12, the formula take far longer to solve. while this range isslightly different from the results of the full dataset (0.05 ≤ Q ≤ 0.13) This canbe explained by the reduced dataset.Figure 5(b) appears to shows that for all values of Q < 0.05 or Q > 0.12,almost all the formulas finish in approximately zero seconds, however this is onlybecause of the scale, in reality while a large number of them do complete veryquickly, in less than one second, numerous other results take varying amountsof time anywhere between zero and 900 seconds (the timeout).The data collected from each result is as follows: number of variables, numberof clauses, number of communities, Q metric, result and time, Prior to analyseswe ensured the quality of the experiments by checking that we had a gooddistribution of results in both the SAT and UNSAT categories, and that in boththere was a reasonable distribution across time.

While we did discover a moreeven distribution of time in the case of the UNSAT vs SAT formula, it is notenough to affect the results. Similarly, while the majority of the results are inthe lower end of the scale, this confirms the result that for the majority of therange of Q, most SAT instances are relatively easy to solve. Once the distributionof SAT vs UNSAT was determined, Q was plotted against time for all resultsFigure 5(c). From this plots we see a very clear trend in the relationship betweenQ and solution time, namely that when 0.05 ≤ Q ≤ 0.13 there is a significantincrease in average solution time. A more clear representation of these results isFigure 5(a), which plots Q on the x-axis against the average execution time ofthe formulas on the y-axis.In addition to the result showing that when 0.05 ≤ Q ≤ 0.13 the formula ishard, we also noticed several interesting features of these graphs.

From thesegraphs we made several observations; Firstly, when looking at the full dataset asshown in Figure 5(c), it can be seen that none of the 2500 formula with a Q < 0.05had a solve time of > 100ms. Secondly, while not immediately clear from lookingat Figure 5(c) we discovered that none of the SAT formula had a Q < 0.1096,while we think it would be possible to generate a satisfiable formula that had a Qvalue in this range, it does not typically occur in randomly generated instances.Bottomline Result: The basic takehome message here is that, when we accounted for potential bias in the generation process and eliminated instances thatwere quick to solve, we got the following result: randomly-generated instanceswith Q values in the range 0.05 ≤ Q ≤ 0.12 (for the reduced set of instancesuniformly binned for Q values ranging from 0 to 0.9 in increments of 0.1) wereunsually hard for MiniSAT to solve compared to instances outside this range,and this result only depends on the Q value and not on any other factor such asnumber of variables or clauses.4Related WorkIn [3] Levy et al introduced the concept of SAT problems having communitystructure.

The paper showed that numerous problems in the SAT 2010 racecontained very high modularity compared to graphs of any other nature. It wasalso suggested in this paper that SAT solvers are able to exploit this hiddenstructure in order to achieve good solve times. However, the paper was unableto explain what characteristics of community structure leads to poor or goodsolve times. Also, in [4] the authors state that while SAT solvers have shownimprovements in solve times for numerous industrial applications, their has beenless success in improving the solve time of randomly generated instances. Theyposit that this is due to the lack of structure present in randomly generatedinstances.In [16] Xu et al describe a SAT solver that chooses its algorithms based on48 features of the input formula.