Structural properties of CNF formulas are often suggested as a basis for explaining the large variation in solving hardness or as instance features that could be exploited by solvers. Examples include community structure and tree-width of graphs associated with the formulas. We will describe some preliminary findings from an experimental exploration of the relevance of these properties to actual performance of CDCL SAT solvers.

This is joint work with S. Jamali and R. McBride. This work was supported by NSERC Discovery and USRA grants.