@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@inproceedings{mull-sat16,
  author    = {Nathan Mull and Daniel J. Fremont and Sanjit A. Seshia},
  title     = {On the Hardness of {SAT} with Community Structure},
 booktitle = {Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT)},
 month = "July",
 year = {2016},
 pages = {141--159},
 abstract = {Recent attempts to explain the effectiveness of Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) on large industrial benchmarks have focused on the concept of community structure. 
Specifically, industrial benchmarks have been empirically found to have good community structure, and experiments seem to show a correlation between such structure and the efficiency of CDCL. 
However, in this paper we establish hardness results suggesting that community structure is not sufficient to explain the success of CDCL in practice. 
First, we formally characterize a property shared by a wide class of metrics capturing community structure, including ``modularity''. 
Next, we show that the SAT instances with good community structure according to any metric with this property are still NP-hard. 
Finally, we also prove that with high probability, random unsatisfiable modular instances generated from the ``pseudo-industrial'' community attachment model of Gir\'aldez-Cru and Levy have exponentially long resolution proofs. 
Such instances are therefore hard for CDCL on average, indicating that actual industrial instances easily solved by CDCL may have some other relevant structure not captured by this model.},
}