Looking for motivated students (undergrads and grads) interested in working on embedded software and systems research. Mail Sebastian Fischmeister for further information.
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) |
Pagination | 252-268 |
Conference Location | Vienna, Austria |
Abstract | 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. |
Notes | (best student paper award) |
Refereed Designation | Refereed |