On the Hardness of SAT with Community Structure

Nathan Mull, Daniel J. Fremont, and Sanjit A. Seshia. On the Hardness of SAT with Community Structure. In Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 141–159, July 2016.

Download

[pdf] 

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áldez-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.

BibTeX

@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.},
}

Generated by bib2html.pl (written by Patrick Riley ) on Thu Jan 12, 2017 16:01:14