|Title||Impact of Community Structure on SAT Solver Performance|
|Publication Type||Conference Paper|
|Year of Publication||2014|
|Authors||Newsham, Z., VI. Ganesh, S. Fischmeister, G. Audemard, and L. Simon|
|Conference Name||17th International Conference on Theory and Applications of Satisfiability Testing (SAT)|
|Conference Location||Vienna, Austria|
Modern CDCL SAT solvers routinely solve very large industrial SAT instances in relatively short periods of time. It is clear that these solvers somehow exploit the structure of real-world instances. However, to-date there have been few results that precisely characterise this structure. In this paper, we provide evidence that the community structure of real-world SAT instances is correlated with the running time of CDCL SAT solvers. It has been known for some time that real-world SAT instances, viewed as graphs, have natural communities in them. A community is a sub-graph of the graph of a SAT instance, such that this sub-graph has more internal edges than outgoing to the rest of the graph. The community structure of a graph is often characterised by a quality metric called Q. Intuitively, a graph with high-quality community structure (high Q) is easily separable into smaller communities, while the one with low Q is not.
(best student paper award)