An SMT Approach to Fractional Hypertree Width

Abstract

Bounded fractional hypertree width ( Open image in new window ) is the most general known structural property that guarantees polynomial-time solvability of the constraint satisfaction problem. Bounded Open image in new window generalizes other structural properties like bounded induced width and bounded hypertree width.

We propose, implement and test the first practical algorithm for computing the Open image in new window and its associated structural decomposition. We provide an extensive empirical evaluation of our method on a large class of benchmark instances which also provides a comparison with known exact decomposition methods for hypertree width. Our approach is based on an efficient encoding of the decomposition problem to SMT (SAT modulo Theory) with Linear Arithmetic as implemented in the SMT solver Open image in new window . The encoding is further strengthened by preprocessing and symmetry breaking methods. Our experiments show (i) that Open image in new window can indeed be computed exactly for a wide range of benchmark instances, and (ii) that state-of-the art SMT techniques can be successfully applied for structural decomposition.