Treewidth in Industrial SAT Benchmarks

  • Robert Mateescu

MSR-TR-2011-22 |

The Boolean Satisfiability (SAT) solvers have been in recent
years very successful at solving very large practical problems,
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 anywhere
close to the worst case upper bound that is known for
graphical models algorithms (e.g., join-tree clustering or variable
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.