Guiding SAT diagnosis with tree decompositions

Abstract

A tree decomposition of a hypergraph is a construction that captures the graph's topological structure. Every tree decomposition has an associated tree width, which can be viewed as a measure of how tree-like the original hypergraph is. Tree decomposition has proven to be a very useful theoretical vehicle for generating polynomial algorithms for subclasses of problems whose general solution is NP-complete. As a rule, this is done by designing the algorithms so that their runtime is bounded by some polynomial times a function of the tree width of a tree decomposition of the original problem. Problem instances that have bounded tree width can thus be solved by the resulting algorithms in polynomial time. A variety of methods are known for deciding satisfiability of Boolean formulas whose hypergraph representations have tree decompositions of small width. However, satisfiability methods based on tree decomposition has yet to make an large impact. In this paper, we report on our effort to learn whether the theoretical applicability of tree decomposition to SAT can be made to work in practice. We discuss how we generate tree decompositions, and how we make use of them to guide variable selection and conflict clause generation. We also present experimental results demonstrating that the method we propose can decrease the number of necessary decisions by one or more orders of magnitude. © Springer-Verlag 2004.