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. We provide three results based on empirical data which show that community structure of real-world industrial instances is a better predictor of the running time of CDCL solvers than other commonly considered factors such as variables and clauses. First, we show that there is a strong correlation between the Q value and Literal Block Distance metric of quality of conflict clauses used in clause-deletion policies in Glucose-like solvers. Second, using regression analysis, we show that the the number of communities and the Q value of the graph of real-world SAT instances is more predictive of the running time of CDCL solvers than traditional metrics like number of variables or clauses. Finally, we show that randomly-generated SAT instances with 0.05 <= Q <= 0.13 are dramatically harder to solve for CDCL solvers than otherwise. |
Year | DOI | Venue |
---|---|---|
2014 | 10.1007/978-3-319-09284-3_20 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Graph,Discrete mathematics,Community structure,Computer science,Regression analysis,Boolean satisfiability problem,Metric (mathematics),Separable space,Exploit | Conference | 8561 |
ISSN | Citations | PageRank |
0302-9743 | 20 | 0.82 |
References | Authors | |
9 | 5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Zack Newsham | 1 | 46 | 3.03 |
Vijay Ganesh | 2 | 1563 | 94.66 |
Sebastian Fischmeister | 3 | 20 | 0.82 |
Gilles Audemard | 4 | 640 | 37.66 |
Laurent Simon | 5 | 746 | 43.15 |