On the Hardness of SAT with Community Structure
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, we have established hardness results suggesting that community structure is not sufficient to explain the success of CDCL in practice. First, we have formally characterized a property shared by a wide class of metrics capturing community structure, including "modularity". Next, we have shown that the SAT instances with good community structure according to any metric with this property are still NP-hard. Finally, we have also proved 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.