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

While they did use certain graph theoreticconcepts, such as node-degree statistics, they did not consider the concept ofcommunities as a feature of the input. The list of 48 features could be used in amore comprehensive model than the ones used in our regression. In [10] Habetet al present an empirical study of the effect of conflict analyses on solution timein CDCL solvers.In [2] the authors present a the notion of fractal dimensions in SAT solvers,they have discovered that as the SAT solver progresses the fractal dimensionincreases when new learnt clauses are added to the formula. They have also discovered that learnt clauses do not connect distant parts of the formula (oneswith long shortest paths between nodes), as one would expect. This is interesting when combined with the work we present stating that clauses which arecomprised of variables in a small number of communities are more useful to thesolver. This means that even when a learnt clause that does connect distantvariable in the formula is added, it is not as useful as a clause that connectslocally occurring variables.5ConclusionsIn this paper we presented evidence that the community structure present in realworld SAT instances is correlated with solution time of CDCL SAT solvers.

First,we highlighted a relationship between Literal Block Distance (LBD), a measureindicating the importance of a learnt clause in CDCL solver, and communitystructure. In particular, learnt clauses that are shared by few communities arehighly correlated with high-quality learnt clauses with low LBD scores.

In otherwords, we have a new measure (number of communities shared by a learnt clause)of quality of learnt clauses that correlates with a very successful existing one(LBD). This result provides new insights into the efficiency of the LBD measureand should be considered to improve solver performance. Second, we introduceda model, that while not perfect, is a first step towards a predictive model forthe solution time of SAT instances. Finally, we presented a result showing thatrandomly generated instances are particularly difficult to solve, regardless ofnumber of clauses or variables, when their modularity is between 0.05 and 0.13.6Future WorkAs mentioned in Section 3.4, our regression is one of the early predictive modelfor solve time of a CDCL solver based on community structure. However, thereare many other factors not discussed in this paper that may play an importantrole in determining solve time, factors such as: median/mean size of clauses,the number of clauses that feature a subset of variables that appear together inanother clause, the number of unique pairs of variables appearing in a clause, orthe size of the largest clique in the variable graph.

Any or all of these featuresmay play a role in determining solution time. In the future we intend to exploreas many of these, and as many of the 48 features from [16] as necessary toimprove our model. Another potential for research is implementing a solver thattakes advantage of community structure to improve solve time, this could beimplemented in several ways, one of which is to create a clause deletion heuristicbased on the community structure (as opposed to LBD deletion policy). Anothercould be to implement a decision heuristic that chooses variables that appearin learnt clauses with variables from very few number of communities. The ideabeing the more local a conflict clause is to a community, the higher its quality.References1.

2013 sat competition. http://satcompetition.org/2013/. Accessed: 2014-01-31.2. Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, and Jordi Levy. Thefractal dimension of sat formulas. arXiv preprint arXiv:1308.5046, 2013.3. Carlos Ansótegui, Jesús Giráldez-Cru, and Jordi Levy.

The community structureof sat formulas. In Theory and Applications of Satisfiability Testing–SAT 2012,pages 410–423. Springer, 2012.4. Carlos Ansótegui and Jordi Levy. On the modularity of industrial sat instances.In CCIA, pages 11–20, 2011.5. Gilles Audemard and Laurent Simon.

Predicting learnt clauses quality in modernSAT solvers. In proceedings of IJCAI, pages 399–404, 2009.6. Aaron Clauset, Mark EJ Newman, and Cristopher Moore. Finding communitystructure in very large networks. Physical review E, 70(6):066111, 2004.7. Niklas Eén and Niklas Sörensson. An extensible sat-solver. In Theory and applications of satisfiability testing, pages 502–518. Springer, 2004.8. Niklas Een and Niklas Sörensson.

Minisat: A sat solver with conflict-clause minimization. Sat, 5, 2005.9. Ian P Gent and Toby Walsh. The sat phase transition. In ECAI, pages 105–109.PITMAN, 1994.10. Djamal Habet and Donia Toumi. Empirical study of the behavior of conflict analysis in cdcl solvers. In Principles and Practice of Constraint Programming, pages678–693.

Springer, 2013.11. David Mitchell, Bart Selman, and Hector Levesque. Hard and easy distributionsof sat problems. In AAAI, volume 92, pages 459–465. Citeseer, 1992.12. Mark EJ Newman. Fast algorithm for detecting community structure in networks.Physical review E, 69(6):066133, 2004.13. Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, and Laurent Simon. Community Structure of SAT Instances Webpage with Data and Code.https://ece.uwaterloo.ca/~vganesh/satcommunitystructure.html.14. Knot Pipatsrisawat and Adnan Darwiche.

A lightweight component caching schemefor satisfiability solvers. In proceedings of SAT, pages 294–299, 2008.15. Moshe Vardi. Phase transition and computation complexity. http://www.lsv.ens-cachan.fr/Events/fmt2012/SLIDES/moshevardi.pdf, 2012.16. Lin Xu, Frank Hutter, Holger H Hoos, and Kevin Leyton-Brown.

Satzilla: Portfoliobased algorithm selection for sat. J. Artif. Intell. Res.(JAIR), 32:565–606, 2008.17. Wangsheng Zhang, Gang Pan, Zhaohui Wu, and Shijian Li. Online communitydetection for large complex networks. In Proceedings of the Twenty-Third international joint conference on Artificial Intelligence, pages 1903–1909. AAAI Press,2013.7AppendixFactor|CO||CL| Q QCOR|CL| Q|CL| Q |CO| QCOR V CLR|CL| Q |CO|Q QCORQQ |CO| QCORQ |CO||V | QCOR|CL| |V | V CLR|CL| |V | QCOR V CLR|V |QCOR|CL| |V | QCOR(Intercept)|CL| QCOR|CL| |V |QCOR V CLRV CLR|CL||V | QCOR V CLR|V | V CLR|CL| |V | Q QCOR|CL| |V | Q|CL| |V | Q |CO||CL| |V | Q |CO| QCOREstimate-1.237e+00-4.226e+02-2.137e+02-1.177e+03-6.024e+023.415e+021.726e+029.451e+024.839e+02-3.177e+01-1.263e+01-2.521e+01-1.376e+01-1.057e+012.096e+01-4.949e+009.486e+009.641e+009.035e+004.452e+004.299e+001.700e+018.059e+00-4.680e+02-2.373e+02-6.594e+02-1.286e+03Std.

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.0009472.927e+023.229 0.0012921.503e+023.220 0.0013351.004e+01 -3.164 0.0016174.503e+00 -2.805 0.0051639.008e+00 -2.798 0.0052634.947e+00 -2.782 0.0055263.912e+00 -2.701 0.0070657.894e+002.656 0.0080731.950e+00 -2.538 0.0113273.792e+002.502 0.0125563.933e+002.451 0.0144563.789e+002.385 0.0173231.892e+002.353 0.0188451.894e+002.270 0.0235077.556e+002.250 0.0247553.811e+002.115 0.0347692.298e+02 -2.036 0.0420601.167e+02 -2.034 0.0422683.315e+02 -1.989 0.0470426.469e+02 -1.988 0.047160Sig*************************************************Table 2: List of all significant effects, three stars indicates the highest level ofconfidence that the effect is important.

indicates an interaction between twoor more factors and Sig stands for Significance.