Treewidth in Industrial SAT Benchmarks

The Boolean Satisfiability (SAT) solvers have been in recent years very successful at solving very large practical prob-lems, with hundreds of thousands of variables and millions of clauses. Although SAT can be viewed as a graphical model, it is intriguing that SAT solvers do not seem to perform any-where close to the worst case upper bound that is known for graphical models algorithms (e.g., join-tree clustering or vari-able elimination), which are exponential in the treewidth of the primal graph. In this paper we empirically investigate the correlation between the treewidth of industrial SAT instances from the SAT2009 competition, and their practical hardness as given by the solving time